{-# 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 {
      forall c tv r f. RTypeF c tv r f -> tv
_rtf_var   :: !tv
    , forall c tv r f. RTypeF c tv r f -> r
_rtf_reft   :: !r
    }

  | RFunF  {
      forall c tv r f. RTypeF c tv r f -> Symbol
_rtf_bind   :: !F.Symbol
    , forall c tv r f. RTypeF c tv r f -> RFInfo
_rtf_rinfo  :: !RFInfo
    , forall c tv r f. RTypeF c tv r f -> f
_rtf_in     :: !f
    , forall c tv r f. RTypeF c tv r f -> f
_rtf_out    :: !f
    , _rtf_reft   :: !r
    }
  | RAllTF {
      forall c tv r f. RTypeF c tv r f -> RTVU c tv
_rtf_tvbind :: !(RTVU c tv) -- RTVar tv (RType c tv ()))
    , forall c tv r f. RTypeF c tv r f -> f
_rtf_ty     :: !f
    , forall c tv r f. RTypeF c tv r f -> r
_rtf_ref    :: !r
    }

  -- | "forall x y <z :: Nat, w :: Int> . TYPE"
  --               ^^^^^^^^^^^^^^^^^^^ (rtf_pvbind)
  | RAllPF {
      forall c tv r f. RTypeF c tv r f -> PVU c tv
_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  {
      forall c tv r f. RTypeF c tv r f -> c
_rtf_tycon  :: !c
    , forall c tv r f. RTypeF c tv r f -> [f]
_rtf_args   :: ![f]
    , forall c tv r f. RTypeF c tv r f -> [RTPropF c tv f]
_rtf_pargs  :: ![RTPropF c tv f]
    , _rtf_reft   :: !r
    }

  | RAllEF {
      _rtf_bind   :: !F.Symbol
    , forall c tv r f. RTypeF c tv r f -> f
_rtf_allarg :: !f
    , _rtf_ty     :: !f
    }

  | RExF {
      _rtf_bind   :: !F.Symbol
    , forall c tv r f. RTypeF c tv r f -> f
_rtf_exarg  :: !f
    , _rtf_ty     :: !f
    }

  | RExprArgF (F.Located F.Expr)

  | RAppTyF{
      forall c tv r f. RTypeF c tv r f -> f
_rtf_arg   :: !f
    , forall c tv r f. RTypeF c tv r f -> f
_rtf_res   :: !f
    , _rtf_reft  :: !r
    }

  | RRTyF  {
      forall c tv r f. RTypeF c tv r f -> [(Symbol, f)]
_rtf_env   :: ![(F.Symbol, f)]
    , _rtf_ref   :: !r
    , forall c tv r f. RTypeF c tv r f -> Oblig
_rtf_obl   :: !Oblig
    , _rtf_ty    :: !f
    }

  | RHoleF r
  deriving ((forall a b. (a -> b) -> RTypeF c tv r a -> RTypeF c tv r b)
-> (forall a b. a -> RTypeF c tv r b -> RTypeF c tv r a)
-> Functor (RTypeF c tv r)
forall a b. a -> RTypeF c tv r b -> RTypeF c tv r a
forall a b. (a -> b) -> RTypeF c tv r a -> RTypeF c tv r b
forall c tv r a b. a -> RTypeF c tv r b -> RTypeF c tv r a
forall c tv r a b. (a -> b) -> RTypeF c tv r a -> RTypeF c tv r b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall c tv r a b. (a -> b) -> RTypeF c tv r a -> RTypeF c tv r b
fmap :: forall a b. (a -> b) -> RTypeF c tv r a -> RTypeF c tv r b
$c<$ :: forall c tv r a b. a -> RTypeF c tv r b -> RTypeF c tv r a
<$ :: forall a b. a -> RTypeF c tv r b -> RTypeF c tv r a
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 :: SpecType -> SpecTypeF SpecType
project (RVar RTyVar
var RReft
reft            ) = RTyVar -> RReft -> SpecTypeF SpecType
forall c tv r f. tv -> r -> RTypeF c tv r f
RVarF RTyVar
var RReft
reft
project (RFun Symbol
bind RFInfo
i SpecType
tin SpecType
tout RReft
reft) = Symbol
-> RFInfo -> SpecType -> SpecType -> RReft -> SpecTypeF SpecType
forall c tv r f. Symbol -> RFInfo -> f -> f -> r -> RTypeF c tv r f
RFunF  Symbol
bind RFInfo
i SpecType
tin SpecType
tout RReft
reft
project (RAllT RTVUV Symbol RTyCon RTyVar
tvbind SpecType
ty RReft
ref      ) = RTVUV Symbol RTyCon RTyVar
-> SpecType -> RReft -> SpecTypeF SpecType
forall c tv r f. RTVU c tv -> f -> r -> RTypeF c tv r f
RAllTF RTVUV Symbol RTyCon RTyVar
tvbind SpecType
ty RReft
ref
project (RAllP PVUV Symbol RTyCon RTyVar
pvbind SpecType
ty          ) = PVUV Symbol RTyCon RTyVar -> SpecType -> SpecTypeF SpecType
forall c tv r f. PVU c tv -> f -> RTypeF c tv r f
RAllPF PVUV Symbol RTyCon RTyVar
pvbind SpecType
ty
project (RApp RTyCon
c [SpecType]
args [RTProp RTyCon RTyVar RReft]
pargs RReft
reft   ) = RTyCon
-> [SpecType]
-> [RTProp RTyCon RTyVar RReft]
-> RReft
-> SpecTypeF SpecType
forall c tv r f.
c -> [f] -> [RTPropF c tv f] -> r -> RTypeF c tv r f
RAppF RTyCon
c [SpecType]
args [RTProp RTyCon RTyVar RReft]
pargs RReft
reft
project (RAllE Symbol
bind SpecType
allarg SpecType
ty     ) = Symbol -> SpecType -> SpecType -> SpecTypeF SpecType
forall c tv r f. Symbol -> f -> f -> RTypeF c tv r f
RAllEF Symbol
bind SpecType
allarg SpecType
ty
project (REx   Symbol
bind SpecType
exarg  SpecType
ty     ) = Symbol -> SpecType -> SpecType -> SpecTypeF SpecType
forall c tv r f. Symbol -> f -> f -> RTypeF c tv r f
RExF Symbol
bind SpecType
exarg SpecType
ty
project (RExprArg Located Expr
e               ) = Located Expr -> SpecTypeF SpecType
forall c tv r f. Located Expr -> RTypeF c tv r f
RExprArgF Located Expr
e
project (RAppTy SpecType
arg SpecType
res RReft
reft      ) = SpecType -> SpecType -> RReft -> SpecTypeF SpecType
forall c tv r f. f -> f -> r -> RTypeF c tv r f
RAppTyF SpecType
arg SpecType
res RReft
reft
project (RRTy [(Symbol, SpecType)]
env RReft
ref Oblig
obl SpecType
ty      ) = [(Symbol, SpecType)]
-> RReft -> Oblig -> SpecType -> SpecTypeF SpecType
forall c tv r f.
[(Symbol, f)] -> r -> Oblig -> f -> RTypeF c tv r f
RRTyF [(Symbol, SpecType)]
env RReft
ref Oblig
obl SpecType
ty
project (RHole RReft
r                  ) = RReft -> SpecTypeF SpecType
forall c tv r f. r -> RTypeF c tv r f
RHoleF RReft
r

embed :: SpecTypeF SpecType -> SpecType
embed :: SpecTypeF SpecType -> SpecType
embed (RVarF RTyVar
var RReft
reft            ) = RTyVar -> RReft -> SpecType
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar RTyVar
var RReft
reft
embed (RFunF Symbol
bind RFInfo
i SpecType
tin SpecType
tout RReft
reft) = Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
bind  RFInfo
i SpecType
tin SpecType
tout RReft
reft
embed (RAllTF RTVUV Symbol RTyCon RTyVar
tvbind SpecType
ty RReft
ref      ) = RTVUV Symbol RTyCon RTyVar -> SpecType -> RReft -> SpecType
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV Symbol RTyCon RTyVar
tvbind SpecType
ty RReft
ref
embed (RAllPF PVUV Symbol RTyCon RTyVar
pvbind SpecType
ty          ) = PVUV Symbol RTyCon RTyVar -> SpecType -> SpecType
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV Symbol RTyCon RTyVar
pvbind SpecType
ty
embed (RAppF RTyCon
c [SpecType]
args [RTProp RTyCon RTyVar RReft]
pargs RReft
reft   ) = RTyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp RTyCon
c [SpecType]
args [RTProp RTyCon RTyVar RReft]
pargs RReft
reft
embed (RAllEF Symbol
bind SpecType
allarg SpecType
ty     ) = Symbol -> SpecType -> SpecType -> SpecType
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE Symbol
bind SpecType
allarg SpecType
ty
embed (RExF   Symbol
bind SpecType
exarg  SpecType
ty     ) = Symbol -> SpecType -> SpecType -> SpecType
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
REx Symbol
bind SpecType
exarg SpecType
ty
embed (RExprArgF Located Expr
e               ) = Located Expr -> SpecType
forall v c tv r. Located (ExprV v) -> RTypeV v c tv r
RExprArg Located Expr
e
embed (RAppTyF SpecType
arg SpecType
res RReft
reft      ) = SpecType -> SpecType -> RReft -> SpecType
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy SpecType
arg SpecType
res RReft
reft
embed (RRTyF [(Symbol, SpecType)]
env RReft
ref Oblig
obl SpecType
ty      ) = [(Symbol, SpecType)] -> RReft -> Oblig -> SpecType -> SpecType
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy [(Symbol, SpecType)]
env RReft
ref Oblig
obl SpecType
ty
embed (RHoleF RReft
r                  ) = RReft -> SpecType
forall v c tv r. r -> RTypeV v c tv r
RHole RReft
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 :: forall a.
SpecType -> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
specTypeToPartial = (RTypeF
   RTyCon
   RTyVar
   RReft
   (SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a))
 -> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a))
-> SpecType -> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
forall {b}. (RTypeF RTyCon RTyVar RReft b -> b) -> SpecType -> b
cata ((SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
 -> Free (RTypeF RTyCon RTyVar RReft) a)
-> RTypeF
     RTyCon
     RTyVar
     RReft
     (SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a))
-> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
forall a b.
(a -> b)
-> RTypeF RTyCon RTyVar RReft a -> RTypeF RTyCon RTyVar RReft b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
-> Free (RTypeF RTyCon RTyVar RReft) a
forall a.
RTypeF RTyCon RTyVar RReft (Free (RTypeF RTyCon RTyVar RReft) a)
-> Free (RTypeF RTyCon RTyVar RReft) a
forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap)
  where
    cata :: (RTypeF RTyCon RTyVar RReft b -> b) -> SpecType -> b
cata RTypeF RTyCon RTyVar RReft b -> b
g = RTypeF RTyCon RTyVar RReft b -> b
g (RTypeF RTyCon RTyVar RReft b -> b)
-> (SpecType -> RTypeF RTyCon RTyVar RReft b) -> SpecType -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SpecType -> b)
-> SpecTypeF SpecType -> RTypeF RTyCon RTyVar RReft b
forall a b.
(a -> b)
-> RTypeF RTyCon RTyVar RReft a -> RTypeF RTyCon RTyVar RReft b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((RTypeF RTyCon RTyVar RReft b -> b) -> SpecType -> b
cata RTypeF RTyCon RTyVar RReft b -> b
g) (SpecTypeF SpecType -> RTypeF RTyCon RTyVar RReft b)
-> (SpecType -> SpecTypeF SpecType)
-> SpecType
-> RTypeF RTyCon RTyVar RReft b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> SpecTypeF SpecType
project

plugType :: SpecType -> PartialSpecType -> SpecType
plugType :: SpecType -> PartialSpecType -> SpecType
plugType SpecType
t = (PartialSpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType)
-> PartialSpecType -> SpecType
forall {a}. (a -> RTypeF RTyCon RTyVar RReft a) -> a -> SpecType
ana ((PartialSpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType)
 -> PartialSpecType -> SpecType)
-> (PartialSpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType)
-> PartialSpecType
-> SpecType
forall a b. (a -> b) -> a -> b
$ \case
    Pure ()
_   -> SpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType
forall a.
SpecType -> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
specTypeToPartial SpecType
t
    Free RTypeF RTyCon RTyVar RReft PartialSpecType
res -> RTypeF RTyCon RTyVar RReft PartialSpecType
res
  where
    ana :: (a -> RTypeF RTyCon RTyVar RReft a) -> a -> SpecType
ana a -> RTypeF RTyCon RTyVar RReft a
g = SpecTypeF SpecType -> SpecType
embed (SpecTypeF SpecType -> SpecType)
-> (a -> SpecTypeF SpecType) -> a -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> SpecType)
-> RTypeF RTyCon RTyVar RReft a -> SpecTypeF SpecType
forall a b.
(a -> b)
-> RTypeF RTyCon RTyVar RReft a -> RTypeF RTyCon RTyVar RReft b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> RTypeF RTyCon RTyVar RReft a) -> a -> SpecType
ana a -> RTypeF RTyCon RTyVar RReft a
g) (RTypeF RTyCon RTyVar RReft a -> SpecTypeF SpecType)
-> (a -> RTypeF RTyCon RTyVar RReft a) -> a -> SpecTypeF SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> RTypeF RTyCon RTyVar RReft a
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 :: SpecType -> ([Symbol], [Symbol])
collectSpecTypeBinders = \case
  RFun Symbol
bind RFInfo
_ SpecType
tin SpecType
tout RReft
_
    | SpecType -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType SpecType
tin -> SpecType -> ([Symbol], [Symbol])
collectSpecTypeBinders SpecType
tout
    | Bool
otherwise       -> let ([Symbol]
bs, [Symbol]
abs') = SpecType -> ([Symbol], [Symbol])
collectSpecTypeBinders SpecType
tout
                          in (Symbol
bind Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
bs, [Symbol]
abs')
  RAllE Symbol
b SpecType
_ SpecType
t ->
    let ([Symbol]
bs, [Symbol]
abs') = SpecType -> ([Symbol], [Symbol])
collectSpecTypeBinders SpecType
t
     in (Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
bs, [Symbol]
abs')
  RAllT (RTVar (RTV TyVar
ab) RTVInfo (RTypeV Symbol RTyCon RTyVar ())
_) SpecType
t RReft
_ ->
    let ([Symbol]
bs, [Symbol]
abs') = SpecType -> ([Symbol], [Symbol])
collectSpecTypeBinders SpecType
t
     in ([Symbol]
bs, TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyVar
ab Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
abs')
  REx Symbol
b SpecType
_ SpecType
t ->
    let ([Symbol]
bs, [Symbol]
abs') = SpecType -> ([Symbol], [Symbol])
collectSpecTypeBinders SpecType
t
     in (Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
bs, [Symbol]
abs')
  RAppTy SpecType
_ SpecType
t RReft
_ -> SpecType -> ([Symbol], [Symbol])
collectSpecTypeBinders SpecType
t
  RRTy [(Symbol, SpecType)]
_ RReft
_ Oblig
_ SpecType
t -> SpecType -> ([Symbol], [Symbol])
collectSpecTypeBinders SpecType
t
  SpecType
_ -> ([], [])

-- 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 :: LHsExpr GhcPs -> SpecType -> LHsExpr GhcPs
buildHsExpr LHsExpr GhcPs
result = SpecType -> LHsExpr GhcPs
SpecType -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
go
  where
    go :: SpecType -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
go = \case
      RFun Symbol
bind RFInfo
_ SpecType
tin SpecType
tout RReft
_
        | SpecType -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType SpecType
tin -> SpecType -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
go SpecType
tout
        | Bool
otherwise       -> [LPat GhcPs] -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (p :: Pass).
(IsPass p, XMG (GhcPass p) (LHsExpr (GhcPass p)) ~ Origin) =>
[LPat (GhcPass p)] -> LHsExpr (GhcPass p) -> LHsExpr (GhcPass p)
mkHsLam [IdP GhcPs -> LPat GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LPat (GhcPass p)
nlVarPat (Symbol -> RdrName
varSymbolToRdrName Symbol
bind)] (SpecType -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
go SpecType
tout)
      RAllE Symbol
_ SpecType
_ SpecType
t -> SpecType -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
go SpecType
t
      RAllT RTVUV Symbol RTyCon RTyVar
_ SpecType
t RReft
_ -> SpecType -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
go SpecType
t
      REx Symbol
_ SpecType
_ SpecType
t -> SpecType -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
go SpecType
t
      RAppTy SpecType
_ SpecType
t RReft
_ -> SpecType -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
go SpecType
t
      RRTy [(Symbol, SpecType)]
_ RReft
_ Oblig
_ SpecType
t -> SpecType -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
go SpecType
t
      SpecType
_ -> LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
result


canonicalizeDictBinder
  :: F.Subable a => [F.Symbol] -> (a, [F.Symbol]) -> (a, [F.Symbol])
canonicalizeDictBinder :: forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [] (a
e', [Symbol]
bs') = (a
e', [Symbol]
bs')
canonicalizeDictBinder [Symbol]
bs (a
e', [] ) = (a
e', [Symbol]
bs)
canonicalizeDictBinder [Symbol]
bs (a
e', [Symbol]
bs') = ([Symbol] -> [Symbol] -> a -> a
forall a. Subable a => [Symbol] -> [Symbol] -> a -> a
renameDictBinder [Symbol]
bs [Symbol]
bs' a
e', [Symbol]
bs)
 where
  renameDictBinder :: (F.Subable a) => [F.Symbol] -> [F.Symbol] -> a -> a
  renameDictBinder :: forall a. Subable a => [Symbol] -> [Symbol] -> a -> a
renameDictBinder []          [Symbol]
_  = a -> a
forall a. a -> a
id
  renameDictBinder [Symbol]
_           [] = a -> a
forall a. a -> a
id
  renameDictBinder [Symbol]
canonicalDs [Symbol]
ds = (Symbol -> Symbol) -> a -> a
forall a. Subable a => (Symbol -> Symbol) -> a -> a
F.substa ((Symbol -> Symbol) -> a -> a) -> (Symbol -> Symbol) -> a -> a
forall a b. (a -> b) -> a -> b
$ \Symbol
x -> Symbol -> Symbol -> HashMap Symbol Symbol -> Symbol
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Symbol
x Symbol
x HashMap Symbol Symbol
tbl
    where tbl :: HashMap Symbol Symbol
tbl = [Char] -> HashMap Symbol Symbol -> HashMap Symbol Symbol
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"TBL" (HashMap Symbol Symbol -> HashMap Symbol Symbol)
-> HashMap Symbol Symbol -> HashMap Symbol Symbol
forall a b. (a -> b) -> a -> b
$ [(Symbol, Symbol)] -> HashMap Symbol Symbol
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
ds [Symbol]
canonicalDs)

elaborateSpecType
  :: (CoreExpr -> F.Expr)
  -> (CoreExpr -> TcRn CoreExpr)
  -> SpecType
  -> TcRn SpecType
elaborateSpecType :: (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr) -> SpecType -> TcRn SpecType
elaborateSpecType CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplifier SpecType
t = TcRn SpecType -> TcRn SpecType
forall a. TcM a -> TcM a
GM.withWiredIn (TcRn SpecType -> TcRn SpecType) -> TcRn SpecType -> TcRn SpecType
forall a b. (a -> b) -> a -> b
$ do
  (t', xs) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> SpecType
-> TcRn (SpecType, [Symbol])
elaborateSpecType' (() -> PartialSpecType
forall a. a -> Free (RTypeF RTyCon RTyVar RReft) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplifier SpecType
t
  case xs of
    Symbol
_ : [Symbol]
_ -> Maybe SrcSpan -> [Char] -> TcRn SpecType
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic
      Maybe SrcSpan
forall a. Maybe a
Nothing
      [Char]
"elaborateSpecType: invariant broken. substitution list for dictionary is not completely consumed"
    [Symbol]
_ -> SpecType -> TcRn SpecType
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SpecType
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' :: PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> SpecType
-> TcRn (SpecType, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify SpecType
t =
  case [Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"elaborateSpecType'" SpecType
t of
    RVar (RTV TyVar
tv) (MkUReft reft :: ReftV Symbol
reft@(F.Reft (Symbol
vv, Expr
_oldE)) PredicateV Symbol
p) -> do
      (ReftV Symbol, SpecType)
-> TcRn (SpecType, [Symbol])
-> ([Symbol] -> Expr -> TcRn (SpecType, [Symbol]))
-> TcRn (SpecType, [Symbol])
forall a.
PPrint a =>
(ReftV Symbol, SpecType)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft
        (ReftV Symbol
reft, SpecType
t)
        ((SpecType, [Symbol]) -> TcRn (SpecType, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SpecType
t, []))
        (\[Symbol]
bs' Expr
ee -> (SpecType, [Symbol]) -> TcRn (SpecType, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RTyVar -> RReft -> SpecType
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar (TyVar -> RTyVar
RTV TyVar
tv) (ReftV Symbol -> PredicateV Symbol -> RReft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ((Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (Symbol
vv, Expr
ee)) PredicateV Symbol
p), [Symbol]
bs'))
        -- YL : Fix
    RFun  Symbol
bind RFInfo
i SpecType
tin SpecType
tout ureft :: RReft
ureft@(MkUReft reft :: ReftV Symbol
reft@(F.Reft (Symbol
vv, Expr
_oldE)) PredicateV Symbol
p) -> do
      -- the reft is never actually used by the child
      -- maybe i should enforce this information at the type level
      let partialFunTp :: PartialSpecType
partialFunTp =
            RTypeF RTyCon RTyVar RReft PartialSpecType -> PartialSpecType
forall (f :: * -> *) a. f (Free f a) -> Free f a
Free (Symbol
-> RFInfo
-> PartialSpecType
-> PartialSpecType
-> RReft
-> RTypeF RTyCon RTyVar RReft PartialSpecType
forall c tv r f. Symbol -> RFInfo -> f -> f -> r -> RTypeF c tv r f
RFunF Symbol
bind RFInfo
i (RTypeF RTyCon RTyVar RReft PartialSpecType -> PartialSpecType
forall a.
RTypeF RTyCon RTyVar RReft (Free (RTypeF RTyCon RTyVar RReft) a)
-> Free (RTypeF RTyCon RTyVar RReft) a
forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap (RTypeF RTyCon RTyVar RReft PartialSpecType -> PartialSpecType)
-> RTypeF RTyCon RTyVar RReft PartialSpecType -> PartialSpecType
forall a b. (a -> b) -> a -> b
$ SpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType
forall a.
SpecType -> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
specTypeToPartial SpecType
tin) (() -> PartialSpecType
forall a. a -> Free (RTypeF RTyCon RTyVar RReft) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) RReft
ureft) :: PartialSpecType
          partialTp' :: PartialSpecType
partialTp' = PartialSpecType
partialTp PartialSpecType -> PartialSpecType -> PartialSpecType
forall a b.
Free (RTypeF RTyCon RTyVar RReft) a
-> Free (RTypeF RTyCon RTyVar RReft) b
-> Free (RTypeF RTyCon RTyVar RReft) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> PartialSpecType
partialFunTp :: PartialSpecType
      (eTin , bs ) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> SpecType
-> TcRn (SpecType, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify SpecType
tin
      (eTout, bs') <- elaborateSpecType' partialTp' coreToLogic simplify tout
      let buildRFunContTrivial
            | SpecType -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType SpecType
tin, Symbol
dictBinder : [Symbol]
bs0' <- [Symbol]
bs' = do
              let (SpecType
eToutRenamed, [Symbol]
canonicalBinders) =
                    [Symbol] -> (SpecType, [Symbol]) -> (SpecType, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (SpecType
eTout, [Symbol]
bs0')
              (SpecType, [Symbol]) -> TcRn (SpecType, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( [Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"RFunTrivial0"
                  (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
dictBinder RFInfo
i SpecType
eTin SpecType
eToutRenamed RReft
ureft
                , [Symbol]
canonicalBinders
                )
            | Bool
otherwise = do
              let (SpecType
eToutRenamed, [Symbol]
canonicalBinders) =
                    [Symbol] -> (SpecType, [Symbol]) -> (SpecType, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (SpecType
eTout, [Symbol]
bs')
              (SpecType, [Symbol]) -> TcRn (SpecType, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( [Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"RFunTrivial1" (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
bind RFInfo
i SpecType
eTin SpecType
eToutRenamed RReft
ureft
                , [Symbol]
canonicalBinders
                )
          buildRFunCont [Symbol]
bs'' Expr
ee
            | SpecType -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType SpecType
tin, Symbol
dictBinder : [Symbol]
bs0' <- [Symbol]
bs' = do
              let (SpecType
eToutRenamed, [Symbol]
canonicalBinders) =
                    [Symbol] -> (SpecType, [Symbol]) -> (SpecType, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (SpecType
eTout, [Symbol]
bs0')
                  (Expr
eeRenamed, [Symbol]
canonicalBinders') =
                    [Symbol] -> (Expr, [Symbol]) -> (Expr, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
canonicalBinders (Expr
ee, [Symbol]
bs'')
              (SpecType, [Symbol]) -> TcRn (SpecType, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
dictBinder RFInfo
i
                       SpecType
eTin
                       SpecType
eToutRenamed
                       (ReftV Symbol -> PredicateV Symbol -> RReft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ((Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (Symbol
vv, Expr
eeRenamed)) PredicateV Symbol
p)
                , [Symbol]
canonicalBinders'
                )
            | Bool
otherwise = do
              let (SpecType
eToutRenamed, [Symbol]
canonicalBinders) =
                    [Symbol] -> (SpecType, [Symbol]) -> (SpecType, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (SpecType
eTout, [Symbol]
bs')
                  (Expr
eeRenamed, [Symbol]
canonicalBinders') =
                    [Symbol] -> (Expr, [Symbol]) -> (Expr, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
canonicalBinders (Expr
ee, [Symbol]
bs'')
              (SpecType, [Symbol]) -> TcRn (SpecType, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
bind RFInfo
i
                       SpecType
eTin
                       SpecType
eToutRenamed
                       (ReftV Symbol -> PredicateV Symbol -> RReft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ((Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (Symbol
vv, Expr
eeRenamed)) PredicateV Symbol
p)
                , [Symbol]
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 RTyVar
tv RTVInfo (RTypeV Symbol RTyCon RTyVar ())
ty) SpecType
tout ureft :: RReft
ureft@(MkUReft ref :: ReftV Symbol
ref@(F.Reft (Symbol
vv, Expr
_oldE)) PredicateV Symbol
p) -> do
      (eTout, bs) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> SpecType
-> TcRn (SpecType, [Symbol])
elaborateSpecType'
        (PartialSpecType
partialTp PartialSpecType -> PartialSpecType -> PartialSpecType
forall a b.
Free (RTypeF RTyCon RTyVar RReft) a
-> Free (RTypeF RTyCon RTyVar RReft) b
-> Free (RTypeF RTyCon RTyVar RReft) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> RTypeF RTyCon RTyVar RReft PartialSpecType -> PartialSpecType
forall (f :: * -> *) a. f (Free f a) -> Free f a
Free (RTVUV Symbol RTyCon RTyVar
-> PartialSpecType
-> RReft
-> RTypeF RTyCon RTyVar RReft PartialSpecType
forall c tv r f. RTVU c tv -> f -> r -> RTypeF c tv r f
RAllTF (RTyVar
-> RTVInfo (RTypeV Symbol RTyCon RTyVar ())
-> RTVUV Symbol RTyCon RTyVar
forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar RTyVar
tv RTVInfo (RTypeV Symbol RTyCon RTyVar ())
ty) (() -> PartialSpecType
forall a. a -> Free (RTypeF RTyCon RTyVar RReft) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) RReft
ureft))
        CoreExpr -> Expr
coreToLogic
        CoreExpr -> TcRn CoreExpr
simplify
        SpecType
tout
      elaborateReft
        (ref, RVar tv mempty)
        (pure (RAllT (RTVar tv ty) eTout ureft, bs))
        (\[Symbol]
bs' Expr
ee ->
          let (Expr
eeRenamed, [Symbol]
canonicalBinders) =
                [Symbol] -> (Expr, [Symbol]) -> (Expr, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (Expr
ee, [Symbol]
bs')
          in  (SpecType, [Symbol]) -> TcRn (SpecType, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( RTVUV Symbol RTyCon RTyVar -> SpecType -> RReft -> SpecType
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT (RTyVar
-> RTVInfo (RTypeV Symbol RTyCon RTyVar ())
-> RTVUV Symbol RTyCon RTyVar
forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar RTyVar
tv RTVInfo (RTypeV Symbol RTyCon RTyVar ())
ty) SpecType
eTout (ReftV Symbol -> PredicateV Symbol -> RReft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ((Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (Symbol
vv, Expr
eeRenamed)) PredicateV Symbol
p)
                , [Symbol]
canonicalBinders
                )
        )
      -- pure (RAllT (RTVar tv ty) eTout ref, bts')
    -- todo: might as well print an error message?
    RAllP PVUV Symbol RTyCon RTyVar
pvbind SpecType
tout -> do
      (eTout, bts') <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> SpecType
-> TcRn (SpecType, [Symbol])
elaborateSpecType'
        (PartialSpecType
partialTp PartialSpecType -> PartialSpecType -> PartialSpecType
forall a b.
Free (RTypeF RTyCon RTyVar RReft) a
-> Free (RTypeF RTyCon RTyVar RReft) b
-> Free (RTypeF RTyCon RTyVar RReft) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> RTypeF RTyCon RTyVar RReft PartialSpecType -> PartialSpecType
forall (f :: * -> *) a. f (Free f a) -> Free f a
Free (PVUV Symbol RTyCon RTyVar
-> PartialSpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType
forall c tv r f. PVU c tv -> f -> RTypeF c tv r f
RAllPF PVUV Symbol RTyCon RTyVar
pvbind (() -> PartialSpecType
forall a. a -> Free (RTypeF RTyCon RTyVar RReft) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())))
        CoreExpr -> Expr
coreToLogic
        CoreExpr -> TcRn CoreExpr
simplify
        SpecType
tout
      pure (RAllP pvbind eTout, bts')
    -- pargs not handled for now
    -- RApp tycon args pargs reft
    RApp RTyCon
tycon [SpecType]
args [RTProp RTyCon RTyVar RReft]
pargs ureft :: RReft
ureft@(MkUReft reft :: ReftV Symbol
reft@(F.Reft (Symbol
vv, Expr
_)) PredicateV Symbol
p)
      | RTyCon -> Bool
forall c. TyConable c => c -> Bool
isClass RTyCon
tycon -> (SpecType, [Symbol]) -> TcRn (SpecType, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SpecType
t, [])
      | Bool
otherwise -> do
        args' <- (SpecType -> TcRn SpecType)
-> [SpecType] -> IOEnv (Env TcGblEnv TcLclEnv) [SpecType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM
          (((SpecType, [Symbol]) -> SpecType)
-> TcRn (SpecType, [Symbol]) -> TcRn SpecType
forall a b.
(a -> b)
-> IOEnv (Env TcGblEnv TcLclEnv) a
-> IOEnv (Env TcGblEnv TcLclEnv) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SpecType, [Symbol]) -> SpecType
forall a b. (a, b) -> a
fst (TcRn (SpecType, [Symbol]) -> TcRn SpecType)
-> (SpecType -> TcRn (SpecType, [Symbol]))
-> SpecType
-> TcRn SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> SpecType
-> TcRn (SpecType, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify)
          [SpecType]
args
        elaborateReft
          (reft, t)
          (pure (RApp tycon args' pargs ureft, []))
          (\[Symbol]
bs' Expr
ee ->
            (SpecType, [Symbol]) -> TcRn (SpecType, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RTyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp RTyCon
tycon [SpecType]
args' [RTProp RTyCon RTyVar RReft]
pargs (ReftV Symbol -> PredicateV Symbol -> RReft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ((Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (Symbol
vv, Expr
ee)) PredicateV Symbol
p), [Symbol]
bs')
          )
    RAppTy SpecType
arg SpecType
res ureft :: RReft
ureft@(MkUReft reft :: ReftV Symbol
reft@(F.Reft (Symbol
vv, Expr
_)) PredicateV Symbol
p) -> do
      (eArg, bs ) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> SpecType
-> TcRn (SpecType, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify SpecType
arg
      (eRes, bs') <- elaborateSpecType' partialTp coreToLogic simplify res
      let (eResRenamed, canonicalBinders) =
            canonicalizeDictBinder bs (eRes, bs')
      elaborateReft
        (reft, t)
        (pure (RAppTy eArg eResRenamed ureft, canonicalBinders))
        (\[Symbol]
bs'' Expr
ee ->
          let (Expr
eeRenamed, [Symbol]
canonicalBinders') =
                [Symbol] -> (Expr, [Symbol]) -> (Expr, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
canonicalBinders (Expr
ee, [Symbol]
bs'')
          in  (SpecType, [Symbol]) -> TcRn (SpecType, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( SpecType -> SpecType -> RReft -> SpecType
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy SpecType
eArg SpecType
eResRenamed (ReftV Symbol -> PredicateV Symbol -> RReft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ((Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (Symbol
vv, Expr
eeRenamed)) PredicateV Symbol
p)
                , [Symbol]
canonicalBinders'
                )
        )
    -- todo: Existential support
    RAllE Symbol
bind SpecType
allarg SpecType
ty -> do
      (eAllarg, bs ) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> SpecType
-> TcRn (SpecType, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify SpecType
allarg
      (eTy    , bs') <- elaborateSpecType' partialTp coreToLogic simplify ty
      let (eTyRenamed, canonicalBinders) = canonicalizeDictBinder bs (eTy, bs')
      pure (RAllE bind eAllarg eTyRenamed, canonicalBinders)
    REx Symbol
bind SpecType
allarg SpecType
ty -> do
      (eAllarg, bs ) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> SpecType
-> TcRn (SpecType, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify SpecType
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 Located Expr
_ -> Maybe SrcSpan -> [Char] -> TcRn (SpecType, [Symbol])
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"RExprArg should not appear here"
    RHole    RReft
_ -> Maybe SrcSpan -> [Char] -> TcRn (SpecType, [Symbol])
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"RHole should not appear here"
    RRTy{}     -> Maybe SrcSpan -> [Char] -> TcRn (SpecType, [Symbol])
forall a. Maybe SrcSpan -> [Char] -> a
todo Maybe SrcSpan
forall a. Maybe a
Nothing ([Char]
"Not sure how to elaborate RRTy" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp SpecType
t)
 where
  boolType :: SpecType
boolType = RTyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp (TyCon -> [PVUV Symbol RTyCon RTyVar] -> TyConInfo -> RTyCon
RTyCon TyCon
boolTyCon [] TyConInfo
defaultTyConInfo) [] [] RReft
forall a. Monoid a => a
mempty :: SpecType
  elaborateReft
    :: (F.PPrint a)
    => (F.Reft, SpecType)
    -> TcRn a
    -> ([F.Symbol] -> F.Expr -> TcRn a)
    -> TcRn a
  elaborateReft :: forall a.
PPrint a =>
(ReftV Symbol, SpecType)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft (reft :: ReftV Symbol
reft@(F.Reft (Symbol
vv, Expr
e)), SpecType
vvTy) TcRn a
trivial [Symbol] -> Expr -> TcRn a
nonTrivialCont =
    if ReftV Symbol -> Bool
isTrivial' ReftV Symbol
reft
      then TcRn a
trivial
      else do
        let
          querySpecType :: SpecType
querySpecType =
            SpecType -> PartialSpecType -> SpecType
plugType (RFInfo -> Symbol -> SpecType -> SpecType -> SpecType
forall r c tv.
Monoid r =>
RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun' (Bool -> RFInfo
classRFInfo Bool
True) Symbol
vv SpecType
vvTy SpecType
boolType) PartialSpecType
partialTp :: SpecType

          ([Symbol]
origBinders, [Symbol]
origTyBinders) = [Char] -> ([Symbol], [Symbol]) -> ([Symbol], [Symbol])
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"collectSpecTypeBinders"
            (([Symbol], [Symbol]) -> ([Symbol], [Symbol]))
-> ([Symbol], [Symbol]) -> ([Symbol], [Symbol])
forall a b. (a -> b) -> a -> b
$ SpecType -> ([Symbol], [Symbol])
collectSpecTypeBinders SpecType
querySpecType



          hsExpr :: LHsExpr GhcPs
hsExpr =
            LHsExpr GhcPs -> SpecType -> LHsExpr GhcPs
buildHsExpr (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr ([Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Symbol]
origBinders) Expr
e)
                        SpecType
querySpecType :: LHsExpr GhcPs
          exprWithTySigs :: GenLocated SrcSpanAnnA (HsExpr GhcPs)
exprWithTySigs = HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs))
-> HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ XExprWithTySig GhcPs
-> LHsExpr GhcPs -> LHsSigWcType (NoGhcTc GhcPs) -> HsExpr GhcPs
forall p.
XExprWithTySig p
-> LHsExpr p -> LHsSigWcType (NoGhcTc p) -> HsExpr p
ExprWithTySig
            XExprWithTySig GhcPs
forall a. NoAnn a => a
noAnn
            LHsExpr GhcPs
hsExpr
            (LHsType GhcPs -> LHsSigWcType GhcPs
hsTypeToHsSigWcType (SpecType -> LHsType GhcPs
specTypeToLHsType SpecType
querySpecType))
        eeWithLamsCore <- LHsExpr GhcPs -> TcRn CoreExpr
GM.elabRnExpr LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
exprWithTySigs
        eeWithLamsCore' <- simplify eeWithLamsCore
        let
          (_, tyBinders) =
            collectSpecTypeBinders
              . ofType
              . exprType
              $ eeWithLamsCore'
          substTy' = [Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
tyBinders [Symbol]
origTyBinders
          eeWithLams =
            CoreExpr -> Expr
coreToLogic ([Char] -> CoreExpr -> CoreExpr
forall a. Outputable a => [Char] -> a -> a
GM.notracePpr [Char]
"eeWithLamsCore" CoreExpr
eeWithLamsCore')
          (bs', ee) = F.notracepp "grabLams" $ grabLams ([], eeWithLams)
          (dictbs, nondictbs) =
            L.partition (F.isPrefixOfSym "$d") bs'
      -- invariant: length nondictbs == length origBinders
          subst = if [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
nondictbs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
origBinders
            then [Char] -> [(Symbol, Symbol)] -> [(Symbol, Symbol)]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"SUBST" ([(Symbol, Symbol)] -> [(Symbol, Symbol)])
-> [(Symbol, Symbol)] -> [(Symbol, Symbol)]
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Symbol] -> [Symbol]
forall a. [a] -> [a]
L.reverse [Symbol]
nondictbs) [Symbol]
origBinders
            else Maybe SrcSpan -> [Char] -> [(Symbol, Symbol)]
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic
              Maybe SrcSpan
forall a. Maybe a
Nothing
              [Char]
"Oops, Ghc gave back more/less binders than I expected"
        ret <- nonTrivialCont
          dictbs
          ( renameBinderCoerc (\Symbol
x -> Symbol -> Maybe Symbol -> Symbol
forall a. a -> Maybe a -> a
Mb.fromMaybe Symbol
x (Symbol -> [(Symbol, Symbol)] -> Maybe Symbol
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Symbol
x [(Symbol, Symbol)]
substTy'))
          . F.substa (\Symbol
x -> Symbol -> Maybe Symbol -> Symbol
forall a. a -> Maybe a -> a
Mb.fromMaybe Symbol
x (Symbol -> [(Symbol, Symbol)] -> Maybe Symbol
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Symbol
x [(Symbol, Symbol)]
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' :: ReftV Symbol -> Bool
isTrivial' (F.Reft (Symbol
_, Expr
F.PTrue)) = Bool
True
  isTrivial' ReftV Symbol
_                     = Bool
False

  grabLams :: ([F.Symbol], F.Expr) -> ([F.Symbol], F.Expr)
  grabLams :: ([Symbol], Expr) -> ([Symbol], Expr)
grabLams ([Symbol]
bs, F.ELam (Symbol
b, Sort
_) Expr
e) = ([Symbol], Expr) -> ([Symbol], Expr)
grabLams (Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
bs, Expr
e)
  grabLams ([Symbol], Expr)
bse                   = ([Symbol], Expr)
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 :: (Symbol -> Symbol) -> Expr -> Expr
renameBinderCoerc Symbol -> Symbol
f = Expr -> Expr
rename
 where
  renameSort :: Sort -> Sort
renameSort = (Symbol -> Symbol) -> Sort -> Sort
renameBinderSort Symbol -> Symbol
f
  rename :: Expr -> Expr
rename e' :: Expr
e'@(F.ESym SymConst
_          ) = Expr
e'
  rename e' :: Expr
e'@(F.ECon Constant
_          ) = Expr
e'
  rename e' :: Expr
e'@(F.EVar Symbol
_          ) = Expr
e'
  rename (   F.EApp Expr
e0 Expr
e1      ) = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
F.EApp (Expr -> Expr
rename Expr
e0) (Expr -> Expr
rename Expr
e1)
  rename (   F.ENeg Expr
e0         ) = Expr -> Expr
forall v. ExprV v -> ExprV v
F.ENeg (Expr -> Expr
rename Expr
e0)
  rename (   F.EBin Bop
bop Expr
e0 Expr
e1  ) = Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
F.EBin Bop
bop (Expr -> Expr
rename Expr
e0) (Expr -> Expr
rename Expr
e1)
  rename (   F.EIte Expr
e0  Expr
e1 Expr
e2  ) = Expr -> Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
F.EIte (Expr -> Expr
rename Expr
e0) (Expr -> Expr
rename Expr
e1) (Expr -> Expr
rename Expr
e2)
  rename (   F.ECst Expr
e' Sort
t       ) = Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
F.ECst (Expr -> Expr
rename Expr
e') (Sort -> Sort
renameSort Sort
t)
  -- rename (F.ELam (x, t) e') = F.ELam (x, renameSort t) (rename e')
  rename (   F.PAnd [Expr]
es         ) = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
F.PAnd (Expr -> Expr
rename (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
  rename (   F.POr  [Expr]
es         ) = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
F.POr (Expr -> Expr
rename (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
  rename (   F.PNot Expr
e'         ) = Expr -> Expr
forall v. ExprV v -> ExprV v
F.PNot (Expr -> Expr
rename Expr
e')
  rename (   F.PImp Expr
e0 Expr
e1      ) = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
F.PImp (Expr -> Expr
rename Expr
e0) (Expr -> Expr
rename Expr
e1)
  rename (   F.PIff Expr
e0 Expr
e1      ) = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
F.PIff (Expr -> Expr
rename Expr
e0) (Expr -> Expr
rename Expr
e1)
  rename (   F.PAtom Brel
brel Expr
e0 Expr
e1) = Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
F.PAtom Brel
brel (Expr -> Expr
rename Expr
e0) (Expr -> Expr
rename Expr
e1)
  rename (F.ECoerc Sort
_ Sort
_ Expr
e') = Expr -> Expr
rename Expr
e'

  rename Expr
e = Maybe SrcSpan -> [Char] -> Expr
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic
    Maybe SrcSpan
forall a. Maybe a
Nothing
    ([Char]
"renameBinderCoerc: Not sure how to handle the expression " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp Expr
e)



renameBinderSort :: (F.Symbol -> F.Symbol) -> F.Sort -> F.Sort
renameBinderSort :: (Symbol -> Symbol) -> Sort -> Sort
renameBinderSort Symbol -> Symbol
f = Sort -> Sort
rename
 where
  rename :: Sort -> Sort
rename Sort
F.FInt             = Sort
F.FInt
  rename Sort
F.FReal            = Sort
F.FReal
  rename Sort
F.FNum             = Sort
F.FNum
  rename Sort
F.FFrac            = Sort
F.FFrac
  rename (   F.FObj Symbol
s     ) = Symbol -> Sort
F.FObj (Symbol -> Symbol
f Symbol
s)
  rename t' :: Sort
t'@(F.FVar Int
_     ) = Sort
t'
  rename (   F.FFunc Sort
t0 Sort
t1) = Sort -> Sort -> Sort
F.FFunc (Sort -> Sort
rename Sort
t0) (Sort -> Sort
rename Sort
t1)
  rename (   F.FAbs  Int
x  Sort
t') = Int -> Sort -> Sort
F.FAbs Int
x (Sort -> Sort
rename Sort
t')
  rename t' :: Sort
t'@(F.FTC FTycon
_      ) = Sort
t'
  rename (   F.FApp Sort
t0 Sort
t1 ) = Sort -> Sort -> Sort
F.FApp (Sort -> Sort
rename Sort
t0) (Sort -> Sort
rename Sort
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 :: HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
_ (F.ECon Constant
c) = Constant -> LHsExpr GhcPs
constantToHsExpr Constant
c
fixExprToHsExpr HashSet Symbol
env (F.EVar Symbol
x)
  | Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Types.[]" =  [Char] -> LHsExpr GhcPs -> LHsExpr GhcPs
forall a. Outputable a => [Char] -> a -> a
GM.notracePpr [Char]
"Empty" (LHsExpr GhcPs -> LHsExpr GhcPs) -> LHsExpr GhcPs -> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
"[]"))
  | Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Types.:" = [Char] -> LHsExpr GhcPs -> LHsExpr GhcPs
forall a. Outputable a => [Char] -> a -> a
GM.notracePpr [Char]
"Cons" (LHsExpr GhcPs -> LHsExpr GhcPs) -> LHsExpr GhcPs -> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
":"))
  | Bool
otherwise = [Char] -> LHsExpr GhcPs -> LHsExpr GhcPs
forall a. Outputable a => [Char] -> a -> a
GM.notracePpr [Char]
"Var" (LHsExpr GhcPs -> LHsExpr GhcPs) -> LHsExpr GhcPs -> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (HashSet Symbol -> Symbol -> RdrName
symbolToRdrName HashSet Symbol
env Symbol
x)
fixExprToHsExpr HashSet Symbol
env (F.EApp Expr
e0 Expr
e1) =
  LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e1)
fixExprToHsExpr HashSet Symbol
env (F.ENeg Expr
e) =
  LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (Name -> RdrName
nameRdrName Name
negateName)) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e)

fixExprToHsExpr HashSet Symbol
env (F.EBin Bop
bop Expr
e0 Expr
e1) = LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
  (LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (Bop -> LHsExpr GhcPs
bopToHsExpr Bop
bop) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0))
  (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e1)
fixExprToHsExpr HashSet Symbol
env (F.EIte Expr
p Expr
e0 Expr
e1) = LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
nlHsIf (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
p)
                                              (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0)
                                              (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e1)

-- FIXME: convert sort to HsType
-- This is currently not doable because how do we know if FInt corresponds to
-- Int or Integer?
fixExprToHsExpr HashSet Symbol
env (F.ECst Expr
e0 Sort
_    ) = HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0
-- fixExprToHsExpr env (F.PAnd []      ) = nlHsVar true_RDR
fixExprToHsExpr HashSet Symbol
_ (F.PAnd []      ) = IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar IdP GhcPs
RdrName
true_RDR
fixExprToHsExpr HashSet Symbol
env (F.PAnd (Expr
e : [Expr]
es)) = (Expr
 -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
 -> GenLocated SrcSpanAnnA (HsExpr GhcPs))
-> GenLocated SrcSpanAnnA (HsExpr GhcPs)
-> [Expr]
-> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
L.foldr Expr -> GenLocated SrcSpanAnnA (HsExpr GhcPs) -> LHsExpr GhcPs
Expr
-> GenLocated SrcSpanAnnA (HsExpr GhcPs)
-> GenLocated SrcSpanAnnA (HsExpr GhcPs)
f (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e) [Expr]
es
 where
  f :: Expr -> GenLocated SrcSpanAnnA (HsExpr GhcPs) -> LHsExpr GhcPs
f Expr
x GenLocated SrcSpanAnnA (HsExpr GhcPs)
acc = LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar IdP GhcPs
RdrName
and_RDR) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
x)) LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
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 HashSet Symbol
env (F.POr [Expr]
es) = LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
  (IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (Module -> FastString -> RdrName
varQual_RDR Module
foldableModule ([Char] -> FastString
fsLit [Char]
"or")))
  ([LHsExpr GhcPs] -> LHsExpr GhcPs
nlList ([LHsExpr GhcPs] -> LHsExpr GhcPs)
-> [LHsExpr GhcPs] -> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env (Expr -> GenLocated SrcSpanAnnA (HsExpr GhcPs))
-> [Expr] -> [GenLocated SrcSpanAnnA (HsExpr GhcPs)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
fixExprToHsExpr HashSet Symbol
env (F.PIff Expr
e0 Expr
e1) = LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
  (LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
"<=>"))) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0)
  )
  (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e1)
fixExprToHsExpr HashSet Symbol
env (F.PNot Expr
e) =
  LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar IdP GhcPs
RdrName
not_RDR) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e)
fixExprToHsExpr HashSet Symbol
env (F.PAtom Brel
brel Expr
e0 Expr
e1) = LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
  (LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (Brel -> LHsExpr GhcPs
brelToHsExpr Brel
brel) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0))
  (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e1)
fixExprToHsExpr HashSet Symbol
env (F.PImp Expr
e0 Expr
e1) = LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
  (LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
"==>"))) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0)
  )
  (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e1)

fixExprToHsExpr HashSet Symbol
_ Expr
e =
  Maybe SrcSpan -> [Char] -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall a. Maybe SrcSpan -> [Char] -> a
todo Maybe SrcSpan
forall a. Maybe a
Nothing ([Char]
"toGhcExpr: Don't know how to handle " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr -> [Char]
forall a. Show a => a -> [Char]
show Expr
e)

constantToHsExpr :: F.Constant -> LHsExpr GhcPs
-- constantToHsExpr (F.I c) = noLoc (HsLit NoExt (HsInt NoExt (mkIntegralLit c)))
constantToHsExpr :: Constant -> LHsExpr GhcPs
constantToHsExpr (F.I Integer
i) =
  HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs))
-> HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ HsOverLit GhcPs -> HsExpr GhcPs
mkHsOverLit (IntegralLit -> HsOverLit GhcPs
mkHsIntegral (Integer -> IntegralLit
forall a. Integral a => a -> IntegralLit
mkIntegralLit Integer
i))
constantToHsExpr (F.R Double
d) =
  HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs))
-> HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ HsOverLit GhcPs -> HsExpr GhcPs
mkHsOverLit (FractionalLit -> HsOverLit GhcPs
mkHsFractional (Rational -> FractionalLit
mkTHFractionalLit (Double -> Rational
forall a. Real a => a -> Rational
toRational Double
d)))
constantToHsExpr Constant
_ =
  Maybe SrcSpan -> [Char] -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall a. Maybe SrcSpan -> [Char] -> a
todo Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"constantToHsExpr: Not sure how to handle constructor L"

-- This probably won't work because of the qualifiers
bopToHsExpr :: F.Bop -> LHsExpr GhcPs
bopToHsExpr :: Bop -> LHsExpr GhcPs
bopToHsExpr Bop
bop = HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (XVar GhcPs -> LIdP GhcPs -> HsExpr GhcPs
forall p. XVar p -> LIdP p -> HsExpr p
HsVar XVar GhcPs
NoExtField
Ghc.noExtField (RdrName -> GenLocated SrcSpanAnnN RdrName
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (Bop -> RdrName
f Bop
bop)))
 where
  f :: Bop -> RdrName
f Bop
F.Plus   = RdrName
plus_RDR
  f Bop
F.Minus  = RdrName
minus_RDR
  f Bop
F.Times  = RdrName
times_RDR
  f Bop
F.Div    = FastString -> RdrName
mkVarUnqual ([Char] -> FastString
fsLit [Char]
"/")
  f Bop
F.Mod    = FastString -> RdrName
GM.prependGHCRealQual ([Char] -> FastString
fsLit [Char]
"mod")
  f Bop
F.RTimes = RdrName
times_RDR
  f Bop
F.RDiv   = FastString -> RdrName
GM.prependGHCRealQual ([Char] -> FastString
fsLit [Char]
"/")

brelToHsExpr :: F.Brel -> LHsExpr GhcPs
brelToHsExpr :: Brel -> LHsExpr GhcPs
brelToHsExpr Brel
brel = HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (XVar GhcPs -> LIdP GhcPs -> HsExpr GhcPs
forall p. XVar p -> LIdP p -> HsExpr p
HsVar XVar GhcPs
NoExtField
Ghc.noExtField (RdrName -> GenLocated SrcSpanAnnN RdrName
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (Brel -> RdrName
f Brel
brel)))
 where
  f :: Brel -> RdrName
f Brel
F.Eq = FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
"==")
  f Brel
F.Gt = RdrName
gt_RDR
  f Brel
F.Lt = RdrName
lt_RDR
  f Brel
F.Ge = RdrName
ge_RDR
  f Brel
F.Le = RdrName
le_RDR
  f Brel
F.Ne = FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
"/=")
  f Brel
_    = Maybe SrcSpan -> [Char] -> RdrName
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"brelToExpr: Unsupported operation"

symbolToRdrNameNs :: NameSpace -> F.Symbol -> RdrName
symbolToRdrNameNs :: NameSpace -> Symbol -> RdrName
symbolToRdrNameNs NameSpace
ns Symbol
x
  | Symbol -> Bool
F.isNonSymbol Symbol
modName = NameSpace -> FastString -> RdrName
mkUnqual NameSpace
ns ([Char] -> FastString
mkFastString (Symbol -> [Char]
F.symbolString Symbol
s))
  | Bool
otherwise = NameSpace -> (FastString, FastString) -> RdrName
mkQual
    NameSpace
ns
    ([Char] -> FastString
mkFastString (Symbol -> [Char]
F.symbolString Symbol
modName), [Char] -> FastString
mkFastString (Symbol -> [Char]
F.symbolString Symbol
s))
  where (Symbol
modName, Symbol
s) = Symbol -> (Symbol, Symbol)
GM.splitModuleName Symbol
x


varSymbolToRdrName :: F.Symbol -> RdrName
varSymbolToRdrName :: Symbol -> RdrName
varSymbolToRdrName = NameSpace -> Symbol -> RdrName
symbolToRdrNameNs NameSpace
varName


-- don't use this function...
symbolToRdrName :: S.HashSet F.Symbol -> F.Symbol -> RdrName
symbolToRdrName :: HashSet Symbol -> Symbol -> RdrName
symbolToRdrName HashSet Symbol
env Symbol
x
  | Symbol -> Bool
F.isNonSymbol Symbol
modName = NameSpace -> FastString -> RdrName
mkUnqual NameSpace
ns ([Char] -> FastString
mkFastString (Symbol -> [Char]
F.symbolString Symbol
s))
  | Bool
otherwise = NameSpace -> (FastString, FastString) -> RdrName
mkQual
    NameSpace
ns
    ([Char] -> FastString
mkFastString (Symbol -> [Char]
F.symbolString Symbol
modName), [Char] -> FastString
mkFastString (Symbol -> [Char]
F.symbolString Symbol
s))
 where
  (Symbol
modName, Symbol
s) = Symbol -> (Symbol, Symbol)
GM.splitModuleName Symbol
x
  ns :: NameSpace
ns | Bool -> Bool
not (Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
x HashSet Symbol
env), Just (Char
c, Symbol
_) <- Symbol -> Maybe (Char, Symbol)
F.unconsSym Symbol
s, Char -> Bool
isUpper Char
c = NameSpace
dataName
     | Bool
otherwise = NameSpace
varName


specTypeToLHsType :: SpecType -> LHsType GhcPs
-- surprised that the type application is necessary
specTypeToLHsType :: SpecType -> LHsType GhcPs
specTypeToLHsType = \case
    RVar (RTV TyVar
tv) RReft
_ -> PromotionFlag -> IdP GhcPs -> LHsType GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
PromotionFlag -> IdP (GhcPass p) -> LHsType (GhcPass p)
nlHsTyVar
      PromotionFlag
NotPromoted
      -- (GM.notracePpr ("varRdr" ++ F.showpp (F.symbol tv)) $ getRdrName tv)
      (NameSpace -> Symbol -> RdrName
symbolToRdrNameNs NameSpace
tvName (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyVar
tv))
    RFun Symbol
_ RFInfo
_ SpecType
tin SpecType
tout RReft
_
      | SpecType -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType SpecType
tin -> HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs))
-> HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall a b. (a -> b) -> a -> b
$ XQualTy GhcPs -> LHsContext GhcPs -> LHsType GhcPs -> HsType GhcPs
forall pass.
XQualTy pass -> LHsContext pass -> LHsType pass -> HsType pass
HsQualTy XQualTy GhcPs
NoExtField
Ghc.noExtField ([GenLocated SrcSpanAnnA (HsType GhcPs)]
-> GenLocated SrcSpanAnnC [GenLocated SrcSpanAnnA (HsType GhcPs)]
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA [SpecType -> LHsType GhcPs
specTypeToLHsType SpecType
tin]) (SpecType -> LHsType GhcPs
specTypeToLHsType SpecType
tout)
      | Bool
otherwise       -> LHsType GhcPs -> LHsType GhcPs -> LHsType GhcPs
forall (p :: Pass).
IsPass p =>
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsFunTy (SpecType -> LHsType GhcPs
specTypeToLHsType SpecType
tin) (SpecType -> LHsType GhcPs
specTypeToLHsType SpecType
tout)
    RAllT (RTVUV Symbol RTyCon RTyVar -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value -> (RTV TyVar
tv)) SpecType
t RReft
_ -> HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs))
-> HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall a b. (a -> b) -> a -> b
$ XForAllTy GhcPs
-> HsForAllTelescope GhcPs -> LHsType GhcPs -> HsType GhcPs
forall pass.
XForAllTy pass
-> HsForAllTelescope pass -> LHsType pass -> HsType pass
HsForAllTy
      XForAllTy GhcPs
NoExtField
Ghc.noExtField
      (EpAnnForallTy
-> [LHsTyVarBndr Specificity GhcPs] -> HsForAllTelescope GhcPs
forall (p :: Pass).
EpAnnForallTy
-> [LHsTyVarBndr Specificity (GhcPass p)]
-> HsForAllTelescope (GhcPass p)
mkHsForAllInvisTele EpAnnForallTy
forall a. NoAnn a => a
noAnn [HsTyVarBndr Specificity GhcPs
-> GenLocated SrcSpanAnnA (HsTyVarBndr Specificity GhcPs)
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (HsTyVarBndr Specificity GhcPs
 -> GenLocated SrcSpanAnnA (HsTyVarBndr Specificity GhcPs))
-> HsTyVarBndr Specificity GhcPs
-> GenLocated SrcSpanAnnA (HsTyVarBndr Specificity GhcPs)
forall a b. (a -> b) -> a -> b
$ XUserTyVar GhcPs
-> Specificity -> LIdP GhcPs -> HsTyVarBndr Specificity GhcPs
forall flag pass.
XUserTyVar pass -> flag -> LIdP pass -> HsTyVarBndr flag pass
UserTyVar [AddEpAnn]
XUserTyVar GhcPs
forall a. NoAnn a => a
noAnn Specificity
SpecifiedSpec (RdrName -> GenLocated SrcSpanAnnN RdrName
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (RdrName -> GenLocated SrcSpanAnnN RdrName)
-> RdrName -> GenLocated SrcSpanAnnN RdrName
forall a b. (a -> b) -> a -> b
$ NameSpace -> Symbol -> RdrName
symbolToRdrNameNs NameSpace
tvName (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyVar
tv))])
      (SpecType -> LHsType GhcPs
specTypeToLHsType SpecType
t)
    RAllP PVUV Symbol RTyCon RTyVar
_ SpecType
ty -> SpecType -> LHsType GhcPs
specTypeToLHsType SpecType
ty
    RApp RTyCon { rtc_tc :: RTyCon -> TyCon
rtc_tc = TyCon
tc } [SpecType]
ts [RTProp RTyCon RTyVar RReft]
_ RReft
_ -> IdP GhcPs -> [LHsType GhcPs] -> LHsType GhcPs
mkHsTyConApp
      (TyCon -> RdrName
forall thing. NamedThing thing => thing -> RdrName
getRdrName TyCon
tc)
      [ SpecType -> LHsType GhcPs
specTypeToLHsType SpecType
t | SpecType
t <- [SpecType]
ts, SpecType -> Bool
forall {v} {c} {tv} {r}. RTypeV v c tv r -> Bool
notExprArg SpecType
t ]
     where
      notExprArg :: RTypeV v c tv r -> Bool
notExprArg (RExprArg Located (ExprV v)
_) = Bool
False
      notExprArg RTypeV v c tv r
_            = Bool
True
    RAllE Symbol
_ SpecType
tin SpecType
tout -> LHsType GhcPs -> LHsType GhcPs -> LHsType GhcPs
forall (p :: Pass).
IsPass p =>
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsFunTy (SpecType -> LHsType GhcPs
specTypeToLHsType SpecType
tin) (SpecType -> LHsType GhcPs
specTypeToLHsType SpecType
tout)
    REx Symbol
_ SpecType
tin SpecType
tout -> LHsType GhcPs -> LHsType GhcPs -> LHsType GhcPs
forall (p :: Pass).
IsPass p =>
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsFunTy (SpecType -> LHsType GhcPs
specTypeToLHsType SpecType
tin) (SpecType -> LHsType GhcPs
specTypeToLHsType SpecType
tout)
    RAppTy SpecType
_ (RExprArg Located Expr
_) RReft
_ ->
      Maybe SrcSpan -> [Char] -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"RExprArg should not appear here"
    RAppTy SpecType
t SpecType
t' RReft
_ -> LHsType GhcPs -> LHsType GhcPs -> LHsType GhcPs
forall (p :: Pass).
IsPass p =>
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsFunTy (SpecType -> LHsType GhcPs
specTypeToLHsType SpecType
t) (SpecType -> LHsType GhcPs
specTypeToLHsType SpecType
t')
    RRTy [(Symbol, SpecType)]
_ RReft
_ Oblig
_ SpecType
t -> SpecType -> LHsType GhcPs
specTypeToLHsType SpecType
t
    RHole RReft
_ -> HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs))
-> HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall a b. (a -> b) -> a -> b
$ XWildCardTy GhcPs -> HsType GhcPs
forall pass. XWildCardTy pass -> HsType pass
HsWildCardTy XWildCardTy GhcPs
NoExtField
Ghc.noExtField
    RExprArg Located Expr
_ ->
      Maybe SrcSpan -> [Char] -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall a. Maybe SrcSpan -> [Char] -> a
todo Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Oops, specTypeToLHsType doesn't know how to handle RExprArg"