{-# LANGUAGE ViewPatterns              #-}
{-# LANGUAGE ExplicitForAll            #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE DeriveFunctor             #-}
{-# LANGUAGE TypeApplications          #-}
{-# LANGUAGE LambdaCase                #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE CPP                       #-}

{-# OPTIONS_GHC -Wno-orphans #-}

{-# OPTIONS_GHC -Wno-dodgy-imports #-} -- TODO(#1913): Fix import of Data.Functor.Foldable.Fix
{-# OPTIONS_GHC -Wno-unused-top-binds #-} -- TODO(#1914): Is RTypeF even used?

-- | 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)
import           Data.Functor.Foldable         hiding (Fix)
#else
import           Data.Functor.Foldable
#endif

import           Data.Char                      ( isUpper )
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 {
      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 ()

type instance Base (RType c tv r) = RTypeF c tv r

instance Recursive (RType c tv r) where
  project :: RType c tv r -> Base (RType c tv r) (RType c tv r)
project (RVar tv
var r
reft            ) = tv -> r -> RTypeF c tv r (RType c tv r)
forall c tv r f. tv -> r -> RTypeF c tv r f
RVarF tv
var r
reft
  project (RFun Symbol
bind RFInfo
i RType c tv r
tin RType c tv r
tout r
reft) = Symbol
-> RFInfo
-> RType c tv r
-> RType c tv r
-> r
-> RTypeF c tv r (RType c tv r)
forall c tv r f. Symbol -> RFInfo -> f -> f -> r -> RTypeF c tv r f
RFunF  Symbol
bind RFInfo
i RType c tv r
tin RType c tv r
tout r
reft
  project (RAllT RTVU c tv
tvbind RType c tv r
ty r
ref      ) = RTVU c tv -> RType c tv r -> r -> RTypeF c tv r (RType c tv r)
forall c tv r f. RTVU c tv -> f -> r -> RTypeF c tv r f
RAllTF RTVU c tv
tvbind RType c tv r
ty r
ref
  project (RAllP PVU c tv
pvbind RType c tv r
ty          ) = PVU c tv -> RType c tv r -> RTypeF c tv r (RType c tv r)
forall c tv r f. PVU c tv -> f -> RTypeF c tv r f
RAllPF PVU c tv
pvbind RType c tv r
ty
  project (RApp c
c [RType c tv r]
args [RTProp c tv r]
pargs r
reft   ) = c
-> [RType c tv r]
-> [RTProp c tv r]
-> r
-> RTypeF c tv r (RType c tv r)
forall c tv r f.
c -> [f] -> [RTPropF c tv f] -> r -> RTypeF c tv r f
RAppF c
c [RType c tv r]
args [RTProp c tv r]
pargs r
reft
  project (RAllE Symbol
bind RType c tv r
allarg RType c tv r
ty     ) = Symbol
-> RType c tv r -> RType c tv r -> RTypeF c tv r (RType c tv r)
forall c tv r f. Symbol -> f -> f -> RTypeF c tv r f
RAllEF Symbol
bind RType c tv r
allarg RType c tv r
ty
  project (REx   Symbol
bind RType c tv r
exarg  RType c tv r
ty     ) = Symbol
-> RType c tv r -> RType c tv r -> RTypeF c tv r (RType c tv r)
forall c tv r f. Symbol -> f -> f -> RTypeF c tv r f
RExF Symbol
bind RType c tv r
exarg RType c tv r
ty
  project (RExprArg Located Expr
e               ) = Located Expr -> RTypeF c tv r (RType c tv r)
forall c tv r f. Located Expr -> RTypeF c tv r f
RExprArgF Located Expr
e
  project (RAppTy RType c tv r
arg RType c tv r
res r
reft      ) = RType c tv r -> RType c tv r -> r -> RTypeF c tv r (RType c tv r)
forall c tv r f. f -> f -> r -> RTypeF c tv r f
RAppTyF RType c tv r
arg RType c tv r
res r
reft
  project (RRTy [(Symbol, RType c tv r)]
env r
ref Oblig
obl RType c tv r
ty      ) = [(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RTypeF c tv r (RType c tv r)
forall c tv r f.
[(Symbol, f)] -> r -> Oblig -> f -> RTypeF c tv r f
RRTyF [(Symbol, RType c tv r)]
env r
ref Oblig
obl RType c tv r
ty
  project (RHole r
r                  ) = r -> RTypeF c tv r (RType c tv r)
forall c tv r f. r -> RTypeF c tv r f
RHoleF r
r

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

-- probably should return spectype instead..
plugType :: SpecType -> PartialSpecType -> SpecType
plugType :: RType RTyCon RTyVar RReft
-> PartialSpecType -> RType RTyCon RTyVar RReft
plugType RType RTyCon RTyVar RReft
t = Fix (RTypeF RTyCon RTyVar RReft) -> RType RTyCon RTyVar RReft
forall s t. (Recursive s, Corecursive t, Base s ~ Base t) => s -> t
refix (Fix (RTypeF RTyCon RTyVar RReft) -> RType RTyCon RTyVar RReft)
-> (PartialSpecType -> Fix (RTypeF RTyCon RTyVar RReft))
-> PartialSpecType
-> RType RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PartialSpecType -> Fix (RTypeF RTyCon RTyVar RReft)
f
 where
  f :: PartialSpecType -> Fix (RTypeF RTyCon RTyVar RReft)
f = (RTypeF RTyCon RTyVar RReft (Fix (RTypeF RTyCon RTyVar RReft))
 -> Fix (RTypeF RTyCon RTyVar RReft))
-> (PartialSpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType)
-> PartialSpecType
-> Fix (RTypeF RTyCon RTyVar RReft)
forall (f :: * -> *) b a.
Functor f =>
(f b -> b) -> (a -> f a) -> a -> b
hylo RTypeF RTyCon RTyVar RReft (Fix (RTypeF RTyCon RTyVar RReft))
-> Fix (RTypeF RTyCon RTyVar RReft)
forall (f :: * -> *). f (Fix f) -> Fix f
Fix ((PartialSpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType)
 -> PartialSpecType -> Fix (RTypeF RTyCon RTyVar RReft))
-> (PartialSpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType)
-> PartialSpecType
-> Fix (RTypeF RTyCon RTyVar RReft)
forall a b. (a -> b) -> a -> b
$ \case
    Pure ()
_   -> RType RTyCon RTyVar RReft
-> RTypeF RTyCon RTyVar RReft PartialSpecType
forall a.
RType RTyCon RTyVar RReft
-> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
specTypeToPartial RType RTyCon RTyVar RReft
t
    Free RTypeF RTyCon RTyVar RReft PartialSpecType
res -> RTypeF RTyCon RTyVar RReft PartialSpecType
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 :: RType RTyCon RTyVar RReft -> ([Symbol], [Symbol])
collectSpecTypeBinders = (Base
   (RType RTyCon RTyVar RReft)
   (RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
 -> ([Symbol], [Symbol]))
-> RType RTyCon RTyVar RReft -> ([Symbol], [Symbol])
forall t a. Recursive t => (Base t (t, a) -> a) -> t -> a
forall a.
(Base (RType RTyCon RTyVar RReft) (RType RTyCon RTyVar RReft, a)
 -> a)
-> RType RTyCon RTyVar RReft -> a
para ((Base
    (RType RTyCon RTyVar RReft)
    (RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
  -> ([Symbol], [Symbol]))
 -> RType RTyCon RTyVar RReft -> ([Symbol], [Symbol]))
-> (Base
      (RType RTyCon RTyVar RReft)
      (RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
    -> ([Symbol], [Symbol]))
-> RType RTyCon RTyVar RReft
-> ([Symbol], [Symbol])
forall a b. (a -> b) -> a -> b
$ \case
  RFunF Symbol
bind RFInfo
_ (RType RTyCon RTyVar RReft
tin, ([Symbol], [Symbol])
_) (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs')) RReft
_ | RType RTyCon RTyVar RReft -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType RTyCon RTyVar RReft
tin -> ([Symbol]
bs, [Symbol]
abs')
                                       | Bool
otherwise       -> (Symbol
bind Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
bs, [Symbol]
abs')
  RAllEF Symbol
b (RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
_ (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs'))  -> (Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
bs, [Symbol]
abs')
  RAllTF (RTVar (RTV TyVar
ab) RTVInfo (RType RTyCon RTyVar ())
_) (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs')) RReft
_ -> ([Symbol]
bs, TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyVar
ab Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
abs')
  RExF Symbol
b (RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
_ (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs'))    -> (Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
bs, [Symbol]
abs')
  RAppTyF (RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
_ (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs')) RReft
_ -> ([Symbol]
bs, [Symbol]
abs')
  RRTyF [(Symbol, (RType RTyCon RTyVar RReft, ([Symbol], [Symbol])))]
_ RReft
_ Oblig
_ (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs')) -> ([Symbol]
bs, [Symbol]
abs')
  Base
  (RType RTyCon RTyVar RReft)
  (RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
_                          -> ([], [])

-- 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 -> RType RTyCon RTyVar RReft -> LHsExpr GhcPs
buildHsExpr LHsExpr GhcPs
result = (Base
   (RType RTyCon RTyVar RReft)
   (RType RTyCon RTyVar RReft, LHsExpr GhcPs)
 -> LHsExpr GhcPs)
-> RType RTyCon RTyVar RReft -> LHsExpr GhcPs
forall t a. Recursive t => (Base t (t, a) -> a) -> t -> a
forall a.
(Base (RType RTyCon RTyVar RReft) (RType RTyCon RTyVar RReft, a)
 -> a)
-> RType RTyCon RTyVar RReft -> a
para ((Base
    (RType RTyCon RTyVar RReft)
    (RType RTyCon RTyVar RReft, LHsExpr GhcPs)
  -> LHsExpr GhcPs)
 -> RType RTyCon RTyVar RReft -> LHsExpr GhcPs)
-> (Base
      (RType RTyCon RTyVar RReft)
      (RType RTyCon RTyVar RReft, LHsExpr GhcPs)
    -> LHsExpr GhcPs)
-> RType RTyCon RTyVar RReft
-> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ \case
  RFunF Symbol
bind RFInfo
_ (RType RTyCon RTyVar RReft
tin, GenLocated SrcSpanAnnA (HsExpr GhcPs)
_) (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res) RReft
_
    | RType RTyCon RTyVar RReft -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType RTyCon RTyVar RReft
tin -> LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
    | 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)] LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
  RAllEF  Symbol
_ (RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsExpr GhcPs))
_        (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res) -> LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
  RAllTF  RTVar RTyVar (RType RTyCon RTyVar ())
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res) RReft
_        -> LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
  RExF    Symbol
_ (RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsExpr GhcPs))
_        (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res) -> LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
  RAppTyF (RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsExpr GhcPs))
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res) RReft
_        -> LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
  RRTyF [(Symbol,
  (RType RTyCon RTyVar RReft,
   GenLocated SrcSpanAnnA (HsExpr GhcPs)))]
_ RReft
_ Oblig
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res)        -> LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
  Base
  (RType RTyCon RTyVar RReft)
  (RType RTyCon RTyVar RReft, LHsExpr GhcPs)
_                           -> LHsExpr 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)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft)
elaborateSpecType CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplifier RType RTyCon RTyVar RReft
t = TcRn (RType RTyCon RTyVar RReft)
-> TcRn (RType RTyCon RTyVar RReft)
forall a. TcM a -> TcM a
GM.withWiredIn (TcRn (RType RTyCon RTyVar RReft)
 -> TcRn (RType RTyCon RTyVar RReft))
-> TcRn (RType RTyCon RTyVar RReft)
-> TcRn (RType RTyCon RTyVar RReft)
forall a b. (a -> b) -> a -> b
$ do
  (RType RTyCon RTyVar RReft
t', [Symbol]
xs) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [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 RType RTyCon RTyVar RReft
t
  case [Symbol]
xs of
    Symbol
_ : [Symbol]
_ -> Maybe SrcSpan -> [Char] -> TcRn (RType RTyCon RTyVar RReft)
forall a. 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]
_ -> RType RTyCon RTyVar RReft -> TcRn (RType RTyCon RTyVar RReft)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure RType RTyCon RTyVar RReft
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)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
t =
  case [Char] -> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"elaborateSpecType'" RType RTyCon RTyVar RReft
t of
    RVar (RTV TyVar
tv) (MkUReft reft :: Reft
reft@(F.Reft (Symbol
vv, Expr
_oldE)) Predicate
p) -> do
      (Reft, RType RTyCon RTyVar RReft)
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
-> ([Symbol] -> Expr -> TcRn (RType RTyCon RTyVar RReft, [Symbol]))
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a.
PPrint a =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft
        (Reft
reft, RType RTyCon RTyVar RReft
t)
        ((RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RType RTyCon RTyVar RReft
t, []))
        (\[Symbol]
bs' Expr
ee -> (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RTyVar -> RReft -> RType RTyCon RTyVar RReft
forall c tv r. tv -> r -> RType c tv r
RVar (TyVar -> RTyVar
RTV TyVar
tv) (Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
ee)) Predicate
p), [Symbol]
bs'))
        -- YL : Fix
    RFun  Symbol
bind RFInfo
i RType RTyCon RTyVar RReft
tin RType RTyCon RTyVar RReft
tout ureft :: RReft
ureft@(MkUReft reft :: Reft
reft@(F.Reft (Symbol
vv, Expr
_oldE)) Predicate
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
$ RType RTyCon RTyVar RReft
-> RTypeF RTyCon RTyVar RReft PartialSpecType
forall a.
RType RTyCon RTyVar RReft
-> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
specTypeToPartial RType RTyCon RTyVar RReft
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
      (RType RTyCon RTyVar RReft
eTin , [Symbol]
bs ) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
tin
      (RType RTyCon RTyVar RReft
eTout, [Symbol]
bs') <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp' CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
tout
      let buildRFunContTrivial :: TcRn (RType RTyCon RTyVar RReft, [Symbol])
buildRFunContTrivial
            | RType RTyCon RTyVar RReft -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType RTyCon RTyVar RReft
tin, Symbol
dictBinder : [Symbol]
bs0' <- [Symbol]
bs' = do
              let (RType RTyCon RTyVar RReft
eToutRenamed, [Symbol]
canonicalBinders) =
                    [Symbol]
-> (RType RTyCon RTyVar RReft, [Symbol])
-> (RType RTyCon RTyVar RReft, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eTout, [Symbol]
bs0')
              (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( [Char] -> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"RFunTrivial0"
                  (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ Symbol
-> RFInfo
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
-> RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
dictBinder RFInfo
i RType RTyCon RTyVar RReft
eTin RType RTyCon RTyVar RReft
eToutRenamed RReft
ureft
                , [Symbol]
canonicalBinders
                )
            | Bool
otherwise = do
              let (RType RTyCon RTyVar RReft
eToutRenamed, [Symbol]
canonicalBinders) =
                    [Symbol]
-> (RType RTyCon RTyVar RReft, [Symbol])
-> (RType RTyCon RTyVar RReft, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eTout, [Symbol]
bs')
              (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( [Char] -> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"RFunTrivial1" (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ Symbol
-> RFInfo
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
-> RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
bind RFInfo
i RType RTyCon RTyVar RReft
eTin RType RTyCon RTyVar RReft
eToutRenamed RReft
ureft
                , [Symbol]
canonicalBinders
                )
          buildRFunCont :: [Symbol] -> Expr -> TcRn (RType RTyCon RTyVar RReft, [Symbol])
buildRFunCont [Symbol]
bs'' Expr
ee
            | RType RTyCon RTyVar RReft -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType RTyCon RTyVar RReft
tin, Symbol
dictBinder : [Symbol]
bs0' <- [Symbol]
bs' = do
              let (RType RTyCon RTyVar RReft
eToutRenamed, [Symbol]
canonicalBinders) =
                    [Symbol]
-> (RType RTyCon RTyVar RReft, [Symbol])
-> (RType RTyCon RTyVar RReft, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
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'')
              (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( Symbol
-> RFInfo
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
-> RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
dictBinder RFInfo
i
                       RType RTyCon RTyVar RReft
eTin
                       RType RTyCon RTyVar RReft
eToutRenamed
                       (Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
eeRenamed)) Predicate
p)
                , [Symbol]
canonicalBinders'
                )
            | Bool
otherwise = do
              let (RType RTyCon RTyVar RReft
eToutRenamed, [Symbol]
canonicalBinders) =
                    [Symbol]
-> (RType RTyCon RTyVar RReft, [Symbol])
-> (RType RTyCon RTyVar RReft, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
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'')
              (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( Symbol
-> RFInfo
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
-> RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
bind RFInfo
i
                       RType RTyCon RTyVar RReft
eTin
                       RType RTyCon RTyVar RReft
eToutRenamed
                       (Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
eeRenamed)) Predicate
p)
                , [Symbol]
canonicalBinders'
                )
      (Reft, RType RTyCon RTyVar RReft)
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
-> ([Symbol] -> Expr -> TcRn (RType RTyCon RTyVar RReft, [Symbol]))
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a.
PPrint a =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft (Reft
reft, RType RTyCon RTyVar RReft
t) TcRn (RType RTyCon RTyVar RReft, [Symbol])
buildRFunContTrivial [Symbol] -> Expr -> TcRn (RType RTyCon RTyVar RReft, [Symbol])
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 (RType RTyCon RTyVar ())
ty) RType RTyCon RTyVar RReft
tout ureft :: RReft
ureft@(MkUReft ref :: Reft
ref@(F.Reft (Symbol
vv, Expr
_oldE)) Predicate
p) -> do
      (RType RTyCon RTyVar RReft
eTout, [Symbol]
bs) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [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 (RTVar RTyVar (RType 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 (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar RTyVar
tv RTVInfo (RType 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
        RType RTyCon RTyVar RReft
tout
      (Reft, RType RTyCon RTyVar RReft)
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
-> ([Symbol] -> Expr -> TcRn (RType RTyCon RTyVar RReft, [Symbol]))
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a.
PPrint a =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft
        (Reft
ref, RTyVar -> RReft -> RType RTyCon RTyVar RReft
forall c tv r. tv -> r -> RType c tv r
RVar RTyVar
tv RReft
forall a. Monoid a => a
mempty)
        ((RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RTVar RTyVar (RType RTyCon RTyVar ())
-> RType RTyCon RTyVar RReft -> RReft -> RType RTyCon RTyVar RReft
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (RTyVar
-> RTVInfo (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar RTyVar
tv RTVInfo (RType RTyCon RTyVar ())
ty) RType RTyCon RTyVar RReft
eTout RReft
ureft, [Symbol]
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  (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( RTVar RTyVar (RType RTyCon RTyVar ())
-> RType RTyCon RTyVar RReft -> RReft -> RType RTyCon RTyVar RReft
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (RTyVar
-> RTVInfo (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar RTyVar
tv RTVInfo (RType RTyCon RTyVar ())
ty) RType RTyCon RTyVar RReft
eTout (Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
eeRenamed)) Predicate
p)
                , [Symbol]
canonicalBinders
                )
        )
      -- pure (RAllT (RTVar tv ty) eTout ref, bts')
    -- todo: might as well print an error message?
    RAllP PVU RTyCon RTyVar
pvbind RType RTyCon RTyVar RReft
tout -> do
      (RType RTyCon RTyVar RReft
eTout, [Symbol]
bts') <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [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 (PVU RTyCon RTyVar
-> PartialSpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType
forall c tv r f. PVU c tv -> f -> RTypeF c tv r f
RAllPF PVU 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
        RType RTyCon RTyVar RReft
tout
      (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PVU RTyCon RTyVar
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU RTyCon RTyVar
pvbind RType RTyCon RTyVar RReft
eTout, [Symbol]
bts')
    -- pargs not handled for now
    -- RApp tycon args pargs reft
    RApp RTyCon
tycon [RType RTyCon RTyVar RReft]
args [RTProp RTyCon RTyVar RReft]
pargs ureft :: RReft
ureft@(MkUReft reft :: Reft
reft@(F.Reft (Symbol
vv, Expr
_)) Predicate
p)
      | RTyCon -> Bool
forall c. TyConable c => c -> Bool
isClass RTyCon
tycon -> (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RType RTyCon RTyVar RReft
t, [])
      | Bool
otherwise -> do
        [RType RTyCon RTyVar RReft]
args' <- (RType RTyCon RTyVar RReft -> TcRn (RType RTyCon RTyVar RReft))
-> [RType RTyCon RTyVar RReft]
-> IOEnv (Env TcGblEnv TcLclEnv) [RType RTyCon RTyVar RReft]
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
          (((RType RTyCon RTyVar RReft, [Symbol])
 -> RType RTyCon RTyVar RReft)
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft)
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 (RType RTyCon RTyVar RReft, [Symbol]) -> RType RTyCon RTyVar RReft
forall a b. (a, b) -> a
fst (TcRn (RType RTyCon RTyVar RReft, [Symbol])
 -> TcRn (RType RTyCon RTyVar RReft))
-> (RType RTyCon RTyVar RReft
    -> TcRn (RType RTyCon RTyVar RReft, [Symbol]))
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify)
          [RType RTyCon RTyVar RReft]
args
        (Reft, RType RTyCon RTyVar RReft)
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
-> ([Symbol] -> Expr -> TcRn (RType RTyCon RTyVar RReft, [Symbol]))
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a.
PPrint a =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft
          (Reft
reft, RType RTyCon RTyVar RReft
t)
          ((RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RTyCon
-> [RType RTyCon RTyVar RReft]
-> [RTProp RTyCon RTyVar RReft]
-> RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
tycon [RType RTyCon RTyVar RReft]
args' [RTProp RTyCon RTyVar RReft]
pargs RReft
ureft, []))
          (\[Symbol]
bs' Expr
ee ->
            (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RTyCon
-> [RType RTyCon RTyVar RReft]
-> [RTProp RTyCon RTyVar RReft]
-> RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
tycon [RType RTyCon RTyVar RReft]
args' [RTProp RTyCon RTyVar RReft]
pargs (Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
ee)) Predicate
p), [Symbol]
bs')
          )
    RAppTy RType RTyCon RTyVar RReft
arg RType RTyCon RTyVar RReft
res ureft :: RReft
ureft@(MkUReft reft :: Reft
reft@(F.Reft (Symbol
vv, Expr
_)) Predicate
p) -> do
      (RType RTyCon RTyVar RReft
eArg, [Symbol]
bs ) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
arg
      (RType RTyCon RTyVar RReft
eRes, [Symbol]
bs') <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
res
      let (RType RTyCon RTyVar RReft
eResRenamed, [Symbol]
canonicalBinders) =
            [Symbol]
-> (RType RTyCon RTyVar RReft, [Symbol])
-> (RType RTyCon RTyVar RReft, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eRes, [Symbol]
bs')
      (Reft, RType RTyCon RTyVar RReft)
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
-> ([Symbol] -> Expr -> TcRn (RType RTyCon RTyVar RReft, [Symbol]))
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a.
PPrint a =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft
        (Reft
reft, RType RTyCon RTyVar RReft
t)
        ((RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft -> RReft -> RType RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType RTyCon RTyVar RReft
eArg RType RTyCon RTyVar RReft
eResRenamed RReft
ureft, [Symbol]
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  (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft -> RReft -> RType RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType RTyCon RTyVar RReft
eArg RType RTyCon RTyVar RReft
eResRenamed (Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
eeRenamed)) Predicate
p)
                , [Symbol]
canonicalBinders'
                )
        )
    -- todo: Existential support
    RAllE Symbol
bind RType RTyCon RTyVar RReft
allarg RType RTyCon RTyVar RReft
ty -> do
      (RType RTyCon RTyVar RReft
eAllarg, [Symbol]
bs ) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
allarg
      (RType RTyCon RTyVar RReft
eTy    , [Symbol]
bs') <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
ty
      let (RType RTyCon RTyVar RReft
eTyRenamed, [Symbol]
canonicalBinders) = [Symbol]
-> (RType RTyCon RTyVar RReft, [Symbol])
-> (RType RTyCon RTyVar RReft, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eTy, [Symbol]
bs')
      (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Symbol
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
bind RType RTyCon RTyVar RReft
eAllarg RType RTyCon RTyVar RReft
eTyRenamed, [Symbol]
canonicalBinders)
    REx Symbol
bind RType RTyCon RTyVar RReft
allarg RType RTyCon RTyVar RReft
ty -> do
      (RType RTyCon RTyVar RReft
eAllarg, [Symbol]
bs ) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
allarg
      (RType RTyCon RTyVar RReft
eTy    , [Symbol]
bs') <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
ty
      let (RType RTyCon RTyVar RReft
eTyRenamed, [Symbol]
canonicalBinders) = [Symbol]
-> (RType RTyCon RTyVar RReft, [Symbol])
-> (RType RTyCon RTyVar RReft, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eTy, [Symbol]
bs')
      (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Symbol
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx Symbol
bind RType RTyCon RTyVar RReft
eAllarg RType RTyCon RTyVar RReft
eTyRenamed, [Symbol]
canonicalBinders)
    -- YL: might need to filter RExprArg out and replace RHole with ghc wildcard
    -- in the future
    RExprArg Located Expr
_ -> Maybe SrcSpan
-> [Char] -> TcRn (RType RTyCon RTyVar RReft, [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 (RType RTyCon RTyVar RReft, [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 (RType RTyCon RTyVar RReft, [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]
++ RType RTyCon RTyVar RReft -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp RType RTyCon RTyVar RReft
t)
 where
  boolType :: RType RTyCon RTyVar RReft
boolType = RTyCon
-> [RType RTyCon RTyVar RReft]
-> [RTProp RTyCon RTyVar RReft]
-> RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp (TyCon -> [PVU RTyCon RTyVar] -> TyConInfo -> RTyCon
RTyCon TyCon
boolTyCon [] TyConInfo
forall a. Default a => a
def) [] [] 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 =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft (reft :: Reft
reft@(F.Reft (Symbol
vv, Expr
e)), RType RTyCon RTyVar RReft
vvTy) TcRn a
trivial [Symbol] -> Expr -> TcRn a
nonTrivialCont =
    if Reft -> Bool
isTrivial' Reft
reft
      then TcRn a
trivial
      else do
        let
          querySpecType :: RType RTyCon RTyVar RReft
querySpecType =
            RType RTyCon RTyVar RReft
-> PartialSpecType -> RType RTyCon RTyVar RReft
plugType (RFInfo
-> Symbol
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
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 RType RTyCon RTyVar RReft
vvTy RType RTyCon RTyVar RReft
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
$ RType RTyCon RTyVar RReft -> ([Symbol], [Symbol])
collectSpecTypeBinders RType RTyCon RTyVar RReft
querySpecType



          hsExpr :: LHsExpr GhcPs
hsExpr =
            LHsExpr GhcPs -> RType RTyCon RTyVar RReft -> 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)
                        RType RTyCon RTyVar RReft
querySpecType :: LHsExpr GhcPs
          exprWithTySigs :: GenLocated SrcSpanAnnA (HsExpr GhcPs)
exprWithTySigs = HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall a an. a -> LocatedAn an 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
EpAnn [AddEpAnn]
forall a. EpAnn a
noAnn
            LHsExpr GhcPs
hsExpr
            (LHsType GhcPs -> LHsSigWcType GhcPs
hsTypeToHsSigWcType (RType RTyCon RTyVar RReft -> LHsType GhcPs
specTypeToLHsType RType RTyCon RTyVar RReft
querySpecType))
        CoreExpr
eeWithLamsCore <- LHsExpr GhcPs -> TcRn CoreExpr
GM.elabRnExpr LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
exprWithTySigs
        CoreExpr
eeWithLamsCore' <- CoreExpr -> TcRn CoreExpr
simplify CoreExpr
eeWithLamsCore
        let
          ([Symbol]
_, [Symbol]
tyBinders) =
            RType RTyCon RTyVar RReft -> ([Symbol], [Symbol])
collectSpecTypeBinders
              (RType RTyCon RTyVar RReft -> ([Symbol], [Symbol]))
-> (CoreExpr -> RType RTyCon RTyVar RReft)
-> CoreExpr
-> ([Symbol], [Symbol])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> RType RTyCon RTyVar RReft
forall r. Monoid r => Type -> RRType r
ofType
              (Type -> RType RTyCon RTyVar RReft)
-> (CoreExpr -> Type) -> CoreExpr -> RType RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() :: Constraint) => CoreExpr -> Type
CoreExpr -> Type
exprType
              (CoreExpr -> ([Symbol], [Symbol]))
-> CoreExpr -> ([Symbol], [Symbol])
forall a b. (a -> b) -> a -> b
$ CoreExpr
eeWithLamsCore'
          substTy' :: [(Symbol, Symbol)]
substTy' = [Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
tyBinders [Symbol]
origTyBinders
          eeWithLams :: Expr
eeWithLams =
            CoreExpr -> Expr
coreToLogic ([Char] -> CoreExpr -> CoreExpr
forall a. Outputable a => [Char] -> a -> a
GM.notracePpr [Char]
"eeWithLamsCore" CoreExpr
eeWithLamsCore')
          ([Symbol]
bs', Expr
ee) = [Char] -> ([Symbol], Expr) -> ([Symbol], Expr)
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"grabLams" (([Symbol], Expr) -> ([Symbol], Expr))
-> ([Symbol], Expr) -> ([Symbol], Expr)
forall a b. (a -> b) -> a -> b
$ ([Symbol], Expr) -> ([Symbol], Expr)
grabLams ([], Expr
eeWithLams)
          ([Symbol]
dictbs, [Symbol]
nondictbs) =
            (Symbol -> Bool) -> [Symbol] -> ([Symbol], [Symbol])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (Symbol -> Symbol -> Bool
F.isPrefixOfSym Symbol
"$d") [Symbol]
bs'
      -- invariant: length nondictbs == length origBinders
          subst :: [(Symbol, Symbol)]
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. Maybe SrcSpan -> [Char] -> a
panic
              Maybe SrcSpan
forall a. Maybe a
Nothing
              [Char]
"Oops, Ghc gave back more/less binders than I expected"
        a
ret <- [Symbol] -> Expr -> TcRn a
nonTrivialCont
          [Symbol]
dictbs
          ( (Symbol -> Symbol) -> Expr -> Expr
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'))
          (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Symbol) -> Expr -> Expr
forall a. Subable a => (Symbol -> Symbol) -> a -> a
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))
          (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ [Char] -> Expr -> Expr
forall a. PPrint a => [Char] -> a -> a
F.notracepp
              (  [Char]
"elaborated: subst "
              [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(Symbol, Symbol)] -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp [(Symbol, Symbol)]
substTy'
              [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"  "
              [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RType RTyCon RTyVar RReft -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp
                   (Type -> RType RTyCon RTyVar RReft
forall r. Monoid r => Type -> RRType r
ofType (Type -> RType RTyCon RTyVar RReft)
-> Type -> RType RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => CoreExpr -> Type
CoreExpr -> Type
exprType CoreExpr
eeWithLamsCore' :: SpecType)
              )
              Expr
ee
          )  -- (GM.dropModuleUnique <$> bs')
        a -> TcRn a
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> a -> a
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"result" a
ret)
                           -- (F.substa )
  isTrivial' :: F.Reft -> Bool
  isTrivial' :: Reft -> Bool
isTrivial' (F.Reft (Symbol
_, Expr
F.PTrue)) = Bool
True
  isTrivial' Reft
_                     = 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
F.EApp (Expr -> Expr
rename Expr
e0) (Expr -> Expr
rename Expr
e1)
  rename (   F.ENeg Expr
e0         ) = Expr -> Expr
F.ENeg (Expr -> Expr
rename Expr
e0)
  rename (   F.EBin Bop
bop Expr
e0 Expr
e1  ) = Bop -> Expr -> Expr -> Expr
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
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
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
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
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
F.PNot (Expr -> Expr
rename Expr
e')
  rename (   F.PImp Expr
e0 Expr
e1      ) = Expr -> Expr -> Expr
F.PImp (Expr -> Expr
rename Expr
e0) (Expr -> Expr
rename Expr
e1)
  rename (   F.PIff Expr
e0 Expr
e1      ) = Expr -> Expr -> Expr
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
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. 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)


mkHsTyConApp ::  IdP GhcPs -> [LHsType GhcPs] -> LHsType GhcPs
mkHsTyConApp :: IdP GhcPs -> [LHsType GhcPs] -> LHsType GhcPs
mkHsTyConApp IdP GhcPs
tyconId [LHsType GhcPs]
tyargs = PromotionFlag
-> LexicalFixity
-> IdP GhcPs
-> [LHsTypeArg GhcPs]
-> LHsType GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
PromotionFlag
-> LexicalFixity
-> IdP (GhcPass p)
-> [LHsTypeArg (GhcPass p)]
-> LHsType (GhcPass p)
nlHsTyConApp PromotionFlag
NotPromoted LexicalFixity
Prefix IdP GhcPs
tyconId ((GenLocated SrcSpanAnnA (HsType GhcPs)
 -> HsArg
      (GenLocated SrcSpanAnnA (HsType GhcPs))
      (GenLocated SrcSpanAnnA (HsType GhcPs)))
-> [GenLocated SrcSpanAnnA (HsType GhcPs)]
-> [HsArg
      (GenLocated SrcSpanAnnA (HsType GhcPs))
      (GenLocated SrcSpanAnnA (HsType GhcPs))]
forall a b. (a -> b) -> [a] -> [b]
map GenLocated SrcSpanAnnA (HsType GhcPs)
-> HsArg
     (GenLocated SrcSpanAnnA (HsType GhcPs))
     (GenLocated SrcSpanAnnA (HsType GhcPs))
forall tm ty. tm -> HsArg tm ty
HsValArg [LHsType GhcPs]
[GenLocated SrcSpanAnnA (HsType GhcPs)]
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 :: 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
dATA_FOLDABLE ([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 a an. a -> LocatedAn an a
noLocA (XOverLitE GhcPs -> HsOverLit GhcPs -> HsExpr GhcPs
forall p. XOverLitE p -> HsOverLit p -> HsExpr p
HsOverLit XOverLitE GhcPs
EpAnn NoEpAnns
forall a. EpAnn a
noAnn (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 a an. a -> LocatedAn an a
noLocA (XOverLitE GhcPs -> HsOverLit GhcPs -> HsExpr GhcPs
forall p. XOverLitE p -> HsOverLit p -> HsExpr p
HsOverLit XOverLitE GhcPs
EpAnn NoEpAnns
forall a. EpAnn a
noAnn (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 a an. a -> LocatedAn an 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 a an. a -> LocatedAn an 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 a an. a -> LocatedAn an 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 a an. a -> LocatedAn an 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 :: RType RTyCon RTyVar RReft -> LHsType GhcPs
specTypeToLHsType =
  ((RTypeF
    RTyCon
    RTyVar
    RReft
    (RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsType GhcPs))
  -> GenLocated SrcSpanAnnA (HsType GhcPs))
 -> (RType RTyCon RTyVar RReft
     -> RTypeF
          RTyCon RTyVar RReft (Identity (RType RTyCon RTyVar RReft)))
 -> RType RTyCon RTyVar RReft
 -> LHsType GhcPs)
-> (RType RTyCon RTyVar RReft
    -> RTypeF
         RTyCon RTyVar RReft (Identity (RType RTyCon RTyVar RReft)))
-> (RTypeF
      RTyCon
      RTyVar
      RReft
      (RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsType GhcPs))
    -> GenLocated SrcSpanAnnA (HsType GhcPs))
-> RType RTyCon RTyVar RReft
-> LHsType GhcPs
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((forall c.
 RTypeF RTyCon RTyVar RReft (RType RTyCon RTyVar RReft, c)
 -> (RType RTyCon RTyVar RReft, RTypeF RTyCon RTyVar RReft c))
-> (forall d.
    Identity (RTypeF RTyCon RTyVar RReft d)
    -> RTypeF RTyCon RTyVar RReft (Identity d))
-> (RTypeF
      RTyCon
      RTyVar
      RReft
      (RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsType GhcPs))
    -> GenLocated SrcSpanAnnA (HsType GhcPs))
-> (RType RTyCon RTyVar RReft
    -> RTypeF
         RTyCon RTyVar RReft (Identity (RType RTyCon RTyVar RReft)))
-> RType RTyCon RTyVar RReft
-> GenLocated SrcSpanAnnA (HsType GhcPs)
forall (w :: * -> *) (f :: * -> *) (m :: * -> *) b a.
(Comonad w, Functor f, Monad m) =>
(forall c. f (w c) -> w (f c))
-> (forall d. m (f d) -> f (m d))
-> (f (w b) -> b)
-> (a -> f (m a))
-> a
-> b
ghylo (forall t a. Corecursive t => Base t (t, a) -> (t, Base t a)
distPara @SpecType) Identity (RTypeF RTyCon RTyVar RReft d)
-> RTypeF RTyCon RTyVar RReft (Identity d)
forall d.
Identity (RTypeF RTyCon RTyVar RReft d)
-> RTypeF RTyCon RTyVar RReft (Identity d)
forall (f :: * -> *) a.
Functor f =>
Identity (f a) -> f (Identity a)
distAna) ((RType RTyCon RTyVar RReft -> Identity (RType RTyCon RTyVar RReft))
-> RTypeF RTyCon RTyVar RReft (RType RTyCon RTyVar RReft)
-> RTypeF
     RTyCon RTyVar RReft (Identity (RType RTyCon RTyVar RReft))
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 RType RTyCon RTyVar RReft -> Identity (RType RTyCon RTyVar RReft)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RTypeF RTyCon RTyVar RReft (RType RTyCon RTyVar RReft)
 -> RTypeF
      RTyCon RTyVar RReft (Identity (RType RTyCon RTyVar RReft)))
-> (RType RTyCon RTyVar RReft
    -> RTypeF RTyCon RTyVar RReft (RType RTyCon RTyVar RReft))
-> RType RTyCon RTyVar RReft
-> RTypeF
     RTyCon RTyVar RReft (Identity (RType RTyCon RTyVar RReft))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType RTyCon RTyVar RReft
-> Base (RType RTyCon RTyVar RReft) (RType RTyCon RTyVar RReft)
RType RTyCon RTyVar RReft
-> RTypeF RTyCon RTyVar RReft (RType RTyCon RTyVar RReft)
forall t. Recursive t => t -> Base t t
project) ((RTypeF
    RTyCon
    RTyVar
    RReft
    (RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsType GhcPs))
  -> GenLocated SrcSpanAnnA (HsType GhcPs))
 -> RType RTyCon RTyVar RReft -> LHsType GhcPs)
-> (RTypeF
      RTyCon
      RTyVar
      RReft
      (RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsType GhcPs))
    -> GenLocated SrcSpanAnnA (HsType GhcPs))
-> RType RTyCon RTyVar RReft
-> LHsType GhcPs
forall a b. (a -> b) -> a -> b
$ \case
    RVarF (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))
    RFunF Symbol
_ RFInfo
_ (RType RTyCon RTyVar RReft
tin, GenLocated SrcSpanAnnA (HsType GhcPs)
tin') (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
tout) RReft
_
      | RType RTyCon RTyVar RReft -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType RTyCon RTyVar RReft
tin -> HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall a an. a -> LocatedAn an 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)]
-> LocatedAn AnnContext [GenLocated SrcSpanAnnA (HsType GhcPs)]
forall a an. a -> LocatedAn an a
noLocA [GenLocated SrcSpanAnnA (HsType GhcPs)
tin']) LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
tout
      | Bool
otherwise       -> LHsType GhcPs -> LHsType GhcPs -> LHsType GhcPs
forall (p :: Pass).
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsFunTy LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
tin' LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
tout
    RAllTF (RTVar RTyVar (RType RTyCon RTyVar ()) -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value -> (RTV TyVar
tv)) (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
t) RReft
_ -> HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall a an. a -> LocatedAn an 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. EpAnn a
noAnn [HsTyVarBndr Specificity GhcPs
-> LocatedAn AnnListItem (HsTyVarBndr Specificity GhcPs)
forall a an. a -> LocatedAn an a
noLocA (HsTyVarBndr Specificity GhcPs
 -> LocatedAn AnnListItem (HsTyVarBndr Specificity GhcPs))
-> HsTyVarBndr Specificity GhcPs
-> LocatedAn AnnListItem (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 XUserTyVar GhcPs
EpAnn [AddEpAnn]
forall a. EpAnn a
noAnn Specificity
SpecifiedSpec (RdrName -> GenLocated SrcSpanAnnN RdrName
forall a an. a -> LocatedAn an 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))])
      LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
t
    RAllPF PVU RTyCon RTyVar
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
ty)                    -> GenLocated SrcSpanAnnA (HsType GhcPs)
ty
    RAppF RTyCon { rtc_tc :: RTyCon -> TyCon
rtc_tc = TyCon
tc } [(RType RTyCon RTyVar RReft,
  GenLocated SrcSpanAnnA (HsType GhcPs))]
ts [RTPropF
   RTyCon
   RTyVar
   (RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsType GhcPs))]
_ RReft
_ -> IdP GhcPs -> [LHsType GhcPs] -> LHsType GhcPs
mkHsTyConApp
      (TyCon -> RdrName
forall thing. NamedThing thing => thing -> RdrName
getRdrName TyCon
tc)
      [ LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
hst | (RType RTyCon RTyVar RReft
t, GenLocated SrcSpanAnnA (HsType GhcPs)
hst) <- [(RType RTyCon RTyVar RReft,
  GenLocated SrcSpanAnnA (HsType GhcPs))]
ts, RType RTyCon RTyVar RReft -> Bool
forall {c} {tv} {r}. RType c tv r -> Bool
notExprArg RType RTyCon RTyVar RReft
t ]
     where
      notExprArg :: RType c tv r -> Bool
notExprArg (RExprArg Located Expr
_) = Bool
False
      notExprArg RType c tv r
_            = Bool
True
    RAllEF Symbol
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
tin) (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
tout) -> LHsType GhcPs -> LHsType GhcPs -> LHsType GhcPs
forall (p :: Pass).
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsFunTy LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
tin LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
tout
    RExF   Symbol
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
tin) (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
tout) -> LHsType GhcPs -> LHsType GhcPs -> LHsType GhcPs
forall (p :: Pass).
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsFunTy LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
tin LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
tout
    -- impossible
    RAppTyF (RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsType GhcPs))
_ (RExprArg Located Expr
_, GenLocated SrcSpanAnnA (HsType GhcPs)
_) 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"
    RAppTyF (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
t) (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
t') RReft
_ -> LHsType GhcPs -> LHsType GhcPs -> LHsType GhcPs
forall (p :: Pass).
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsAppTy LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
t LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
t'
    -- YL: todo..
    RRTyF [(Symbol,
  (RType RTyCon RTyVar RReft,
   GenLocated SrcSpanAnnA (HsType GhcPs)))]
_ RReft
_ Oblig
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
t)       -> GenLocated SrcSpanAnnA (HsType GhcPs)
t
    RHoleF RReft
_                 -> HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall a an. a -> LocatedAn an 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
    RExprArgF 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"