{-# LANGUAGE ViewPatterns              #-}
{-# LANGUAGE ExplicitForAll            #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE DeriveFunctor             #-}
{-# LANGUAGE LambdaCase                #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE TemplateHaskellQuotes     #-}
{-# LANGUAGE FlexibleContexts          #-}

{-# OPTIONS_GHC -Wno-orphans #-}

-- | This module uses GHC API to elaborate the resolves expressions

-- TODO: Genearlize to BareType and replace the existing resolution mechanisms

module Language.Haskell.Liquid.Bare.Elaborate
  ( fixExprToHsExpr
  , elaborateSpecType
  -- , buildSimplifier
  )
where

import qualified Language.Fixpoint.Types       as F
-- import           Control.Arrow
import           Liquid.GHC.API hiding (panic, varName)
import qualified Language.Haskell.Liquid.GHC.Misc
                                               as GM
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.RefType
                                                ( ofType )
import qualified Data.List                     as L
import qualified Data.HashMap.Strict           as M
import qualified Data.HashSet                  as S
import           Control.Monad.Free

import           Data.Char                      ( isUpper )
import           GHC.Types.Name.Occurrence
import qualified Liquid.GHC.API as Ghc
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 NoReft) f


-- | SpecType with Holes.
--   It provides us a context to construct the ghc queries.
--   I don't think we can reuse RHole since it is not intended
--   for this use case

type SpecTypeF = RTypeF RTyCon RTyVar RReft
type PartialSpecType = Free SpecTypeF ()

project :: SpecType -> SpecTypeF SpecType
project :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
project (RVar RTyVar
var RReft
reft            ) = RTyVar
-> RReft -> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall c tv r f. tv -> r -> RTypeF c tv r f
RVarF RTyVar
var RReft
reft
project (RFun Symbol
bind RFInfo
i RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout RReft
reft) = Symbol
-> RFInfo
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall c tv r f. Symbol -> RFInfo -> f -> f -> r -> RTypeF c tv r f
RFunF  Symbol
bind RFInfo
i RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout RReft
reft
project (RAllT RTVUBV Symbol Symbol RTyCon RTyVar
tvbind RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty RReft
ref      ) = RTVUBV Symbol Symbol RTyCon RTyVar
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall c tv r f. RTVU c tv -> f -> r -> RTypeF c tv r f
RAllTF RTVUBV Symbol Symbol RTyCon RTyVar
tvbind RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty RReft
ref
project (RAllP PVUBV Symbol Symbol RTyCon RTyVar
pvbind RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty          ) = PVUBV Symbol Symbol RTyCon RTyVar
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall c tv r f. PVU c tv -> f -> RTypeF c tv r f
RAllPF PVUBV Symbol Symbol RTyCon RTyVar
pvbind RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty
project (RApp RTyCon
c [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
args [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
pargs RReft
reft   ) = RTyCon
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
-> RReft
-> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall c tv r f.
c -> [f] -> [RTPropF c tv f] -> r -> RTypeF c tv r f
RAppF RTyCon
c [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
args [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
pargs RReft
reft
project (RAllE Symbol
bind RTypeBV Symbol Symbol RTyCon RTyVar RReft
allarg RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty     ) = Symbol
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall c tv r f. Symbol -> f -> f -> RTypeF c tv r f
RAllEF Symbol
bind RTypeBV Symbol Symbol RTyCon RTyVar RReft
allarg RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty
project (REx   Symbol
bind RTypeBV Symbol Symbol RTyCon RTyVar RReft
exarg  RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty     ) = Symbol
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall c tv r f. Symbol -> f -> f -> RTypeF c tv r f
RExF Symbol
bind RTypeBV Symbol Symbol RTyCon RTyVar RReft
exarg RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty
project (RExprArg Located (ExprBV Symbol Symbol)
e               ) = Located (ExprBV Symbol Symbol)
-> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall c tv r f. Located (ExprBV Symbol Symbol) -> RTypeF c tv r f
RExprArgF Located (ExprBV Symbol Symbol)
e
project (RAppTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
arg RTypeBV Symbol Symbol RTyCon RTyVar RReft
res RReft
reft      ) = RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall c tv r f. f -> f -> r -> RTypeF c tv r f
RAppTyF RTypeBV Symbol Symbol RTyCon RTyVar RReft
arg RTypeBV Symbol Symbol RTyCon RTyVar RReft
res RReft
reft
project (RRTy [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
env RReft
ref Oblig
obl RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty      ) = [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> RReft
-> Oblig
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall c tv r f.
[(Symbol, f)] -> r -> Oblig -> f -> RTypeF c tv r f
RRTyF [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
env RReft
ref Oblig
obl RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty
project (RHole RReft
r                  ) = RReft -> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall c tv r f. r -> RTypeF c tv r f
RHoleF RReft
r

embed :: SpecTypeF SpecType -> SpecType
embed :: SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
embed (RVarF RTyVar
var RReft
reft            ) = RTyVar -> RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar RTyVar
var RReft
reft
embed (RFunF Symbol
bind RFInfo
i RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout RReft
reft) = Symbol
-> RFInfo
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
bind  RFInfo
i RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout RReft
reft
embed (RAllTF RTVUBV Symbol Symbol RTyCon RTyVar
tvbind RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty RReft
ref      ) = RTVUBV Symbol Symbol RTyCon RTyVar
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT RTVUBV Symbol Symbol RTyCon RTyVar
tvbind RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty RReft
ref
embed (RAllPF PVUBV Symbol Symbol RTyCon RTyVar
pvbind RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty          ) = PVUBV Symbol Symbol RTyCon RTyVar
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVUBV Symbol Symbol RTyCon RTyVar
pvbind RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty
embed (RAppF RTyCon
c [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
args [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
pargs RReft
reft   ) = RTyCon
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp RTyCon
c [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
args [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
pargs RReft
reft
embed (RAllEF Symbol
bind RTypeBV Symbol Symbol RTyCon RTyVar RReft
allarg RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty     ) = Symbol
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllE Symbol
bind RTypeBV Symbol Symbol RTyCon RTyVar RReft
allarg RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty
embed (RExF   Symbol
bind RTypeBV Symbol Symbol RTyCon RTyVar RReft
exarg  RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty     ) = Symbol
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
REx Symbol
bind RTypeBV Symbol Symbol RTyCon RTyVar RReft
exarg RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty
embed (RExprArgF Located (ExprBV Symbol Symbol)
e               ) = Located (ExprBV Symbol Symbol)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. Located (ExprBV b v) -> RTypeBV b v c tv r
RExprArg Located (ExprBV Symbol Symbol)
e
embed (RAppTyF RTypeBV Symbol Symbol RTyCon RTyVar RReft
arg RTypeBV Symbol Symbol RTyCon RTyVar RReft
res RReft
reft      ) = RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAppTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
arg RTypeBV Symbol Symbol RTyCon RTyVar RReft
res RReft
reft
embed (RRTyF [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
env RReft
ref Oblig
obl RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty      ) = [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> RReft
-> Oblig
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
[(b, RTypeBV b v c tv r)]
-> r -> Oblig -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RRTy [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
env RReft
ref Oblig
obl RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty
embed (RHoleF RReft
r                  ) = RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. r -> RTypeBV b v c tv r
RHole RReft
r


-- specTypeToLHsType :: SpecType -> LHsType GhcPs
-- specTypeToLHsType = typeToLHsType . toType

-- -- Given types like x:a -> y:a -> _, this function returns x:a -> y:a -> Bool
-- -- Free monad takes care of substitution

-- A one-way function. Kind of like injecting something into Maybe
specTypeToPartial :: forall a . SpecType -> SpecTypeF (Free SpecTypeF a)
specTypeToPartial :: forall a.
RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
specTypeToPartial = (RTypeF
   RTyCon
   RTyVar
   RReft
   (RTypeF RTyCon RTyVar RReft (Free (RTypeF RTyCon RTyVar RReft) a))
 -> RTypeF
      RTyCon RTyVar RReft (Free (RTypeF RTyCon RTyVar RReft) a))
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeF RTyCon RTyVar RReft (Free (RTypeF RTyCon RTyVar RReft) a)
forall {b}.
(RTypeF RTyCon RTyVar RReft b -> b)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> b
cata ((RTypeF RTyCon RTyVar RReft (Free (RTypeF RTyCon RTyVar RReft) a)
 -> Free (RTypeF RTyCon RTyVar RReft) a)
-> RTypeF
     RTyCon
     RTyVar
     RReft
     (RTypeF RTyCon RTyVar RReft (Free (RTypeF RTyCon RTyVar RReft) a))
-> RTypeF RTyCon RTyVar RReft (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 RTypeF RTyCon RTyVar RReft (Free (RTypeF RTyCon RTyVar RReft) a)
-> Free (RTypeF RTyCon RTyVar RReft) a
forall a.
RTypeF RTyCon RTyVar RReft (Free (RTypeF RTyCon RTyVar RReft) a)
-> Free (RTypeF RTyCon RTyVar RReft) a
forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap)
  where
    cata :: (RTypeF RTyCon RTyVar RReft b -> b)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> b
cata RTypeF RTyCon RTyVar RReft b -> b
g = RTypeF RTyCon RTyVar RReft b -> b
g (RTypeF RTyCon RTyVar RReft b -> b)
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> RTypeF RTyCon RTyVar RReft b)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> b)
-> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeF RTyCon RTyVar RReft b
forall a b.
(a -> b)
-> RTypeF RTyCon RTyVar RReft a -> RTypeF RTyCon RTyVar RReft b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((RTypeF RTyCon RTyVar RReft b -> b)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> b
cata RTypeF RTyCon RTyVar RReft b -> b
g) (SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> RTypeF RTyCon RTyVar RReft b)
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeF RTyCon RTyVar RReft b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
project

plugType :: SpecType -> PartialSpecType -> SpecType
plugType :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> PartialSpecType -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
plugType RTypeBV Symbol Symbol RTyCon RTyVar RReft
t = (PartialSpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType)
-> PartialSpecType -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall {t}.
(t -> RTypeF RTyCon RTyVar RReft t)
-> t -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
ana ((PartialSpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType)
 -> PartialSpecType -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> (PartialSpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType)
-> PartialSpecType
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ \case
    Pure ()
_   -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeF RTyCon RTyVar RReft PartialSpecType
forall a.
RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
specTypeToPartial RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
    Free RTypeF RTyCon RTyVar RReft PartialSpecType
res -> RTypeF RTyCon RTyVar RReft PartialSpecType
res
  where
    ana :: (t -> RTypeF RTyCon RTyVar RReft t)
-> t -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
ana t -> RTypeF RTyCon RTyVar RReft t
g = SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
embed (SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> (t -> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> t
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeF RTyCon RTyVar RReft t
-> SpecTypeF (RTypeBV Symbol Symbol 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 ((t -> RTypeF RTyCon RTyVar RReft t)
-> t -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
ana t -> RTypeF RTyCon RTyVar RReft t
g) (RTypeF RTyCon RTyVar RReft t
 -> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> (t -> RTypeF RTyCon RTyVar RReft t)
-> t
-> SpecTypeF (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> RTypeF RTyCon RTyVar RReft t
g

-- build the expression we send to ghc for elaboration
-- YL: tweak this function to see if ghc accepts explicit dictionary binders
-- returning both expressions and binders since ghc adds unique id to the expressions

-- | returns (lambda binders, forall binders)
collectSpecTypeBinders :: SpecType -> ([F.Symbol], [F.Symbol])
collectSpecTypeBinders :: RTypeBV Symbol Symbol RTyCon RTyVar RReft -> ([Symbol], [Symbol])
collectSpecTypeBinders = \case
  RFun Symbol
bind RFInfo
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout RReft
_
    | RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> ([Symbol], [Symbol])
collectSpecTypeBinders RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout
    | Bool
otherwise       -> let ([Symbol]
bs, [Symbol]
abs') = RTypeBV Symbol Symbol RTyCon RTyVar RReft -> ([Symbol], [Symbol])
collectSpecTypeBinders RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout
                          in (Symbol
bind Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
bs, [Symbol]
abs')
  RAllE Symbol
b RTypeBV Symbol Symbol RTyCon RTyVar RReft
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t ->
    let ([Symbol]
bs, [Symbol]
abs') = RTypeBV Symbol Symbol RTyCon RTyVar RReft -> ([Symbol], [Symbol])
collectSpecTypeBinders RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
     in (Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
bs, [Symbol]
abs')
  RAllT (RTVar (RTV Var
ab) RTVInfo (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
_) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RReft
_ ->
    let ([Symbol]
bs, [Symbol]
abs') = RTypeBV Symbol Symbol RTyCon RTyVar RReft -> ([Symbol], [Symbol])
collectSpecTypeBinders RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
     in ([Symbol]
bs, Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
ab Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
abs')
  REx Symbol
b RTypeBV Symbol Symbol RTyCon RTyVar RReft
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t ->
    let ([Symbol]
bs, [Symbol]
abs') = RTypeBV Symbol Symbol RTyCon RTyVar RReft -> ([Symbol], [Symbol])
collectSpecTypeBinders RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
     in (Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
bs, [Symbol]
abs')
  RAppTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RReft
_ -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> ([Symbol], [Symbol])
collectSpecTypeBinders RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
  RRTy [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
_ RReft
_ Oblig
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> ([Symbol], [Symbol])
collectSpecTypeBinders RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
  RTypeBV Symbol Symbol RTyCon RTyVar RReft
_ -> ([], [])

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


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

elaborateSpecType
  :: (CoreExpr -> F.Expr)
  -> (CoreExpr -> TcRn CoreExpr)
  -> SpecType
  -> TcRn SpecType
elaborateSpecType :: (CoreExpr -> ExprBV Symbol Symbol)
-> (CoreExpr -> TcRn CoreExpr)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
elaborateSpecType CoreExpr -> ExprBV Symbol Symbol
coreToLogic CoreExpr -> TcRn CoreExpr
simplifier RTypeBV Symbol Symbol RTyCon RTyVar RReft
t = TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall a. TcM a -> TcM a
GM.withWiredIn (TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall a b. (a -> b) -> a -> b
$ do
  (t', xs) <- PartialSpecType
-> (CoreExpr -> ExprBV Symbol Symbol)
-> (CoreExpr -> TcRn CoreExpr)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> TcRn (RTypeBV Symbol Symbol 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 -> ExprBV Symbol Symbol
coreToLogic CoreExpr -> TcRn CoreExpr
simplifier RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
  case xs of
    Symbol
_ : [Symbol]
_ -> Maybe SrcSpan
-> [Char] -> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic
      Maybe SrcSpan
forall a. Maybe a
Nothing
      [Char]
"elaborateSpecType: invariant broken. substitution list for dictionary is not completely consumed"
    [Symbol]
_ -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure RTypeBV Symbol Symbol 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 -> ExprBV Symbol Symbol)
-> (CoreExpr -> TcRn CoreExpr)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> ExprBV Symbol Symbol
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RTypeBV Symbol Symbol RTyCon RTyVar RReft
t =
  case [Char]
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"elaborateSpecType'" RTypeBV Symbol Symbol RTyCon RTyVar RReft
t of
    RVar (RTV Var
tv) (MkUReft reft :: ReftBV Symbol Symbol
reft@(F.Reft (Symbol
vv, ExprBV Symbol Symbol
_oldE)) PredicateBV Symbol Symbol
p) -> do
      (ReftBV Symbol Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
-> ([Symbol]
    -> ExprBV Symbol Symbol
    -> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol]))
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
forall a.
PPrint a =>
(ReftBV Symbol Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> ExprBV Symbol Symbol -> TcRn a) -> TcRn a
elaborateReft
        (ReftBV Symbol Symbol
reft, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
        ((RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RTypeBV Symbol Symbol RTyCon RTyVar RReft
t, []))
        (\[Symbol]
bs' ExprBV Symbol Symbol
ee -> (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RTyVar -> RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar (Var -> RTyVar
RTV Var
tv) (ReftBV Symbol Symbol -> PredicateBV Symbol Symbol -> RReft
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ((Symbol, ExprBV Symbol Symbol) -> ReftBV Symbol Symbol
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (Symbol
vv, ExprBV Symbol Symbol
ee)) PredicateBV Symbol Symbol
p), [Symbol]
bs'))
        -- YL : Fix
    RFun  Symbol
bind RFInfo
i RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout ureft :: RReft
ureft@(MkUReft reft :: ReftBV Symbol Symbol
reft@(F.Reft (Symbol
vv, ExprBV Symbol Symbol
_oldE)) PredicateBV Symbol Symbol
p) -> do
      -- the reft is never actually used by the child
      -- maybe i should enforce this information at the type level
      let partialFunTp :: PartialSpecType
partialFunTp =
            RTypeF RTyCon RTyVar RReft PartialSpecType -> PartialSpecType
forall (f :: * -> *) a. f (Free f a) -> Free f a
Free (Symbol
-> RFInfo
-> PartialSpecType
-> PartialSpecType
-> RReft
-> RTypeF RTyCon RTyVar RReft PartialSpecType
forall c tv r f. Symbol -> RFInfo -> f -> f -> r -> RTypeF c tv r f
RFunF Symbol
bind RFInfo
i (RTypeF RTyCon RTyVar RReft PartialSpecType -> PartialSpecType
forall a.
RTypeF RTyCon RTyVar RReft (Free (RTypeF RTyCon RTyVar RReft) a)
-> Free (RTypeF RTyCon RTyVar RReft) a
forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap (RTypeF RTyCon RTyVar RReft PartialSpecType -> PartialSpecType)
-> RTypeF RTyCon RTyVar RReft PartialSpecType -> PartialSpecType
forall a b. (a -> b) -> a -> b
$ RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeF RTyCon RTyVar RReft PartialSpecType
forall a.
RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
specTypeToPartial RTypeBV Symbol Symbol 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
      (eTin , bs ) <- PartialSpecType
-> (CoreExpr -> ExprBV Symbol Symbol)
-> (CoreExpr -> TcRn CoreExpr)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> ExprBV Symbol Symbol
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin
      (eTout, bs') <- elaborateSpecType' partialTp' coreToLogic simplify tout
      let buildRFunContTrivial
            | RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin, Symbol
dictBinder : [Symbol]
bs0' <- [Symbol]
bs' = do
              let (RTypeBV Symbol Symbol RTyCon RTyVar RReft
eToutRenamed, [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
canonicalBinders) =
                    [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
    [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)])
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
    [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)])
forall a.
(Subable a, PPrint (Variable a), Ord (Variable a)) =>
[Variable a] -> (a, [Variable a]) -> (a, [Variable a])
canonicalizeDictBinder [Symbol]
[Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
bs (RTypeBV Symbol Symbol RTyCon RTyVar RReft
eTout, [Symbol]
[Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
bs0')
              (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( [Char]
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"RFunTrivial0"
                  (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ Symbol
-> RFInfo
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
dictBinder RFInfo
i RTypeBV Symbol Symbol RTyCon RTyVar RReft
eTin RTypeBV Symbol Symbol RTyCon RTyVar RReft
eToutRenamed RReft
ureft
                , [Symbol]
[Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
canonicalBinders
                )
            | Bool
otherwise = do
              let (RTypeBV Symbol Symbol RTyCon RTyVar RReft
eToutRenamed, [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
canonicalBinders) =
                    [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
    [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)])
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
    [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)])
forall a.
(Subable a, PPrint (Variable a), Ord (Variable a)) =>
[Variable a] -> (a, [Variable a]) -> (a, [Variable a])
canonicalizeDictBinder [Symbol]
[Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
bs (RTypeBV Symbol Symbol RTyCon RTyVar RReft
eTout, [Symbol]
[Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
bs')
              (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( [Char]
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"RFunTrivial1" (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ Symbol
-> RFInfo
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
bind RFInfo
i RTypeBV Symbol Symbol RTyCon RTyVar RReft
eTin RTypeBV Symbol Symbol RTyCon RTyVar RReft
eToutRenamed RReft
ureft
                , [Symbol]
[Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
canonicalBinders
                )
          buildRFunCont [Symbol]
bs'' ExprBV Symbol Symbol
ee
            | RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin, Symbol
dictBinder : [Symbol]
bs0' <- [Symbol]
bs' = do
              let (RTypeBV Symbol Symbol RTyCon RTyVar RReft
eToutRenamed, [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
canonicalBinders) =
                    [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
    [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)])
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
    [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)])
forall a.
(Subable a, PPrint (Variable a), Ord (Variable a)) =>
[Variable a] -> (a, [Variable a]) -> (a, [Variable a])
canonicalizeDictBinder [Symbol]
[Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
bs (RTypeBV Symbol Symbol RTyCon RTyVar RReft
eTout, [Symbol]
[Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
bs0')
                  (ExprBV Symbol Symbol
eeRenamed, [Variable (ExprBV Symbol Symbol)]
canonicalBinders') =
                    [Variable (ExprBV Symbol Symbol)]
-> (ExprBV Symbol Symbol, [Variable (ExprBV Symbol Symbol)])
-> (ExprBV Symbol Symbol, [Variable (ExprBV Symbol Symbol)])
forall a.
(Subable a, PPrint (Variable a), Ord (Variable a)) =>
[Variable a] -> (a, [Variable a]) -> (a, [Variable a])
canonicalizeDictBinder [Variable (ExprBV Symbol Symbol)]
[Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
canonicalBinders (ExprBV Symbol Symbol
ee, [Symbol]
[Variable (ExprBV Symbol Symbol)]
bs'')
              (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( Symbol
-> RFInfo
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
dictBinder RFInfo
i
                       RTypeBV Symbol Symbol RTyCon RTyVar RReft
eTin
                       RTypeBV Symbol Symbol RTyCon RTyVar RReft
eToutRenamed
                       (ReftBV Symbol Symbol -> PredicateBV Symbol Symbol -> RReft
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ((Symbol, ExprBV Symbol Symbol) -> ReftBV Symbol Symbol
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (Symbol
vv, ExprBV Symbol Symbol
eeRenamed)) PredicateBV Symbol Symbol
p)
                , [Symbol]
[Variable (ExprBV Symbol Symbol)]
canonicalBinders'
                )
            | Bool
otherwise = do
              let (RTypeBV Symbol Symbol RTyCon RTyVar RReft
eToutRenamed, [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
canonicalBinders) =
                    [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
    [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)])
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
    [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)])
forall a.
(Subable a, PPrint (Variable a), Ord (Variable a)) =>
[Variable a] -> (a, [Variable a]) -> (a, [Variable a])
canonicalizeDictBinder [Symbol]
[Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
bs (RTypeBV Symbol Symbol RTyCon RTyVar RReft
eTout, [Symbol]
[Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
bs')
                  (ExprBV Symbol Symbol
eeRenamed, [Variable (ExprBV Symbol Symbol)]
canonicalBinders') =
                    [Variable (ExprBV Symbol Symbol)]
-> (ExprBV Symbol Symbol, [Variable (ExprBV Symbol Symbol)])
-> (ExprBV Symbol Symbol, [Variable (ExprBV Symbol Symbol)])
forall a.
(Subable a, PPrint (Variable a), Ord (Variable a)) =>
[Variable a] -> (a, [Variable a]) -> (a, [Variable a])
canonicalizeDictBinder [Variable (ExprBV Symbol Symbol)]
[Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
canonicalBinders (ExprBV Symbol Symbol
ee, [Symbol]
[Variable (ExprBV Symbol Symbol)]
bs'')
              (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( Symbol
-> RFInfo
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
bind RFInfo
i
                       RTypeBV Symbol Symbol RTyCon RTyVar RReft
eTin
                       RTypeBV Symbol Symbol RTyCon RTyVar RReft
eToutRenamed
                       (ReftBV Symbol Symbol -> PredicateBV Symbol Symbol -> RReft
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ((Symbol, ExprBV Symbol Symbol) -> ReftBV Symbol Symbol
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (Symbol
vv, ExprBV Symbol Symbol
eeRenamed)) PredicateBV Symbol Symbol
p)
                , [Symbol]
[Variable (ExprBV Symbol Symbol)]
canonicalBinders'
                )
      elaborateReft (reft, t) buildRFunContTrivial buildRFunCont

        -- (\bs' ee | isClassType tin -> do
        --    let eeRenamed = renameDictBinder canonicalBinders bs' ee
        --    pure (RFun bind eTin eToutRenamed (MkUReft (F.Reft (vv, eeRenamed)) p), bs')
        -- )

    -- support for RankNTypes/ref
    RAllT (RTVar RTyVar
tv RTVInfo (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
ty) RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout ureft :: RReft
ureft@(MkUReft ref :: ReftBV Symbol Symbol
ref@(F.Reft (Symbol
vv, ExprBV Symbol Symbol
_oldE)) PredicateBV Symbol Symbol
p) -> do
      (eTout, bs) <- PartialSpecType
-> (CoreExpr -> ExprBV Symbol Symbol)
-> (CoreExpr -> TcRn CoreExpr)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> TcRn (RTypeBV Symbol Symbol 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 (RTVUBV Symbol Symbol RTyCon RTyVar
-> PartialSpecType
-> RReft
-> RTypeF RTyCon RTyVar RReft PartialSpecType
forall c tv r f. RTVU c tv -> f -> r -> RTypeF c tv r f
RAllTF (RTyVar
-> RTVInfo (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
-> RTVUBV Symbol Symbol RTyCon RTyVar
forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar RTyVar
tv RTVInfo (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
ty) (() -> PartialSpecType
forall a. a -> Free (RTypeF RTyCon RTyVar RReft) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) RReft
ureft))
        CoreExpr -> ExprBV Symbol Symbol
coreToLogic
        CoreExpr -> TcRn CoreExpr
simplify
        RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout
      elaborateReft
        (ref, RVar tv mempty)
        (pure (RAllT (RTVar tv ty) eTout ureft, bs))
        (\[Symbol]
bs' ExprBV Symbol Symbol
ee ->
          let (ExprBV Symbol Symbol
eeRenamed, [Variable (ExprBV Symbol Symbol)]
canonicalBinders) =
                [Variable (ExprBV Symbol Symbol)]
-> (ExprBV Symbol Symbol, [Variable (ExprBV Symbol Symbol)])
-> (ExprBV Symbol Symbol, [Variable (ExprBV Symbol Symbol)])
forall a.
(Subable a, PPrint (Variable a), Ord (Variable a)) =>
[Variable a] -> (a, [Variable a]) -> (a, [Variable a])
canonicalizeDictBinder [Symbol]
[Variable (ExprBV Symbol Symbol)]
bs (ExprBV Symbol Symbol
ee, [Symbol]
[Variable (ExprBV Symbol Symbol)]
bs')
          in  (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( RTVUBV Symbol Symbol RTyCon RTyVar
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT (RTyVar
-> RTVInfo (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
-> RTVUBV Symbol Symbol RTyCon RTyVar
forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar RTyVar
tv RTVInfo (RTypeBV Symbol Symbol RTyCon RTyVar NoReft)
ty) RTypeBV Symbol Symbol RTyCon RTyVar RReft
eTout (ReftBV Symbol Symbol -> PredicateBV Symbol Symbol -> RReft
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ((Symbol, ExprBV Symbol Symbol) -> ReftBV Symbol Symbol
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (Symbol
vv, ExprBV Symbol Symbol
eeRenamed)) PredicateBV Symbol Symbol
p)
                , [Symbol]
[Variable (ExprBV Symbol Symbol)]
canonicalBinders
                )
        )
      -- pure (RAllT (RTVar tv ty) eTout ref, bts')
    -- todo: might as well print an error message?
    RAllP PVUBV Symbol Symbol RTyCon RTyVar
pvbind RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout -> do
      (eTout, bts') <- PartialSpecType
-> (CoreExpr -> ExprBV Symbol Symbol)
-> (CoreExpr -> TcRn CoreExpr)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> TcRn (RTypeBV Symbol Symbol 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 (PVUBV Symbol Symbol RTyCon RTyVar
-> PartialSpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType
forall c tv r f. PVU c tv -> f -> RTypeF c tv r f
RAllPF PVUBV Symbol Symbol RTyCon RTyVar
pvbind (() -> PartialSpecType
forall a. a -> Free (RTypeF RTyCon RTyVar RReft) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())))
        CoreExpr -> ExprBV Symbol Symbol
coreToLogic
        CoreExpr -> TcRn CoreExpr
simplify
        RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout
      pure (RAllP pvbind eTout, bts')
    -- pargs not handled for now
    -- RApp tycon args pargs reft
    RApp RTyCon
tycon [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
args [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
pargs ureft :: RReft
ureft@(MkUReft reft :: ReftBV Symbol Symbol
reft@(F.Reft (Symbol
vv, ExprBV Symbol Symbol
_)) PredicateBV Symbol Symbol
p)
      | RTyCon -> Bool
forall c. TyConable c => c -> Bool
isClass RTyCon
tycon -> (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RTypeBV Symbol Symbol RTyCon RTyVar RReft
t, [])
      | Bool
otherwise -> do
        args' <- (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> IOEnv
     (Env TcGblEnv TcLclEnv) [RTypeBV Symbol Symbol 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
          (((RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
-> TcRn (RTypeBV Symbol Symbol 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 (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a, b) -> a
fst (TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
 -> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol]))
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PartialSpecType
-> (CoreExpr -> ExprBV Symbol Symbol)
-> (CoreExpr -> TcRn CoreExpr)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> ExprBV Symbol Symbol
coreToLogic CoreExpr -> TcRn CoreExpr
simplify)
          [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
args
        elaborateReft
          (reft, t)
          (pure (RApp tycon args' pargs ureft, []))
          (\[Symbol]
bs' ExprBV Symbol Symbol
ee ->
            (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RTyCon
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp RTyCon
tycon [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
args' [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
pargs (ReftBV Symbol Symbol -> PredicateBV Symbol Symbol -> RReft
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ((Symbol, ExprBV Symbol Symbol) -> ReftBV Symbol Symbol
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (Symbol
vv, ExprBV Symbol Symbol
ee)) PredicateBV Symbol Symbol
p), [Symbol]
bs')
          )
    RAppTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
arg RTypeBV Symbol Symbol RTyCon RTyVar RReft
res ureft :: RReft
ureft@(MkUReft reft :: ReftBV Symbol Symbol
reft@(F.Reft (Symbol
vv, ExprBV Symbol Symbol
_)) PredicateBV Symbol Symbol
p) -> do
      (eArg, bs ) <- PartialSpecType
-> (CoreExpr -> ExprBV Symbol Symbol)
-> (CoreExpr -> TcRn CoreExpr)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> ExprBV Symbol Symbol
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RTypeBV Symbol Symbol RTyCon RTyVar RReft
arg
      (eRes, bs') <- elaborateSpecType' partialTp coreToLogic simplify res
      let (eResRenamed, canonicalBinders) =
            canonicalizeDictBinder bs (eRes, bs')
      elaborateReft
        (reft, t)
        (pure (RAppTy eArg eResRenamed ureft, canonicalBinders))
        (\[Symbol]
bs'' ExprBV Symbol Symbol
ee ->
          let (ExprBV Symbol Symbol
eeRenamed, [Variable (ExprBV Symbol Symbol)]
canonicalBinders') =
                [Variable (ExprBV Symbol Symbol)]
-> (ExprBV Symbol Symbol, [Variable (ExprBV Symbol Symbol)])
-> (ExprBV Symbol Symbol, [Variable (ExprBV Symbol Symbol)])
forall a.
(Subable a, PPrint (Variable a), Ord (Variable a)) =>
[Variable a] -> (a, [Variable a]) -> (a, [Variable a])
canonicalizeDictBinder [Variable (ExprBV Symbol Symbol)]
[Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
canonicalBinders (ExprBV Symbol Symbol
ee, [Symbol]
[Variable (ExprBV Symbol Symbol)]
bs'')
          in  (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAppTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
eArg RTypeBV Symbol Symbol RTyCon RTyVar RReft
eResRenamed (ReftBV Symbol Symbol -> PredicateBV Symbol Symbol -> RReft
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ((Symbol, ExprBV Symbol Symbol) -> ReftBV Symbol Symbol
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (Symbol
vv, ExprBV Symbol Symbol
eeRenamed)) PredicateBV Symbol Symbol
p)
                , [Symbol]
[Variable (ExprBV Symbol Symbol)]
canonicalBinders'
                )
        )
    -- todo: Existential support
    RAllE Symbol
bind RTypeBV Symbol Symbol RTyCon RTyVar RReft
allarg RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty -> do
      (eAllarg, bs ) <- PartialSpecType
-> (CoreExpr -> ExprBV Symbol Symbol)
-> (CoreExpr -> TcRn CoreExpr)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> ExprBV Symbol Symbol
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RTypeBV Symbol Symbol RTyCon RTyVar RReft
allarg
      (eTy    , bs') <- elaborateSpecType' partialTp coreToLogic simplify ty
      let (eTyRenamed, canonicalBinders) = canonicalizeDictBinder bs (eTy, bs')
      pure (RAllE bind eAllarg eTyRenamed, canonicalBinders)
    REx Symbol
bind RTypeBV Symbol Symbol RTyCon RTyVar RReft
allarg RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty -> do
      (eAllarg, bs ) <- PartialSpecType
-> (CoreExpr -> ExprBV Symbol Symbol)
-> (CoreExpr -> TcRn CoreExpr)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> TcRn (RTypeBV Symbol Symbol RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> ExprBV Symbol Symbol
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RTypeBV Symbol Symbol RTyCon RTyVar RReft
allarg
      (eTy    , bs') <- elaborateSpecType' partialTp coreToLogic simplify ty
      let (eTyRenamed, canonicalBinders) = canonicalizeDictBinder bs (eTy, bs')
      pure (REx bind eAllarg eTyRenamed, canonicalBinders)
    -- YL: might need to filter RExprArg out and replace RHole with ghc wildcard
    -- in the future
    RExprArg Located (ExprBV Symbol Symbol)
_ -> Maybe SrcSpan
-> [Char]
-> TcRn (RTypeBV Symbol Symbol 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 (RTypeBV Symbol Symbol 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 (RTypeBV Symbol Symbol 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]
++ RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
 where
  boolType :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
boolType = RTyCon
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp (TyCon -> [PVUBV Symbol Symbol RTyCon RTyVar] -> TyConInfo -> RTyCon
RTyCon TyCon
boolTyCon [] TyConInfo
defaultTyConInfo) [] [] RReft
forall a. Monoid a => a
mempty :: SpecType
  elaborateReft
    :: (F.PPrint a)
    => (F.Reft, SpecType)
    -> TcRn a
    -> ([F.Symbol] -> F.Expr -> TcRn a)
    -> TcRn a
  elaborateReft :: forall a.
PPrint a =>
(ReftBV Symbol Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> ExprBV Symbol Symbol -> TcRn a) -> TcRn a
elaborateReft (reft :: ReftBV Symbol Symbol
reft@(F.Reft (Symbol
vv, ExprBV Symbol Symbol
e)), RTypeBV Symbol Symbol RTyCon RTyVar RReft
vvTy) TcRn a
trivial [Symbol] -> ExprBV Symbol Symbol -> TcRn a
nonTrivialCont =
    if ReftBV Symbol Symbol -> Bool
isTrivial' ReftBV Symbol Symbol
reft
      then TcRn a
trivial
      else do
        let
          querySpecType :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
querySpecType =
            RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> PartialSpecType -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
plugType (RFInfo
-> Symbol
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r c tv.
IsReft r =>
RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun' (Bool -> RFInfo
classRFInfo Bool
True) Symbol
vv RTypeBV Symbol Symbol RTyCon RTyVar RReft
vvTy RTypeBV Symbol Symbol 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
$ RTypeBV Symbol Symbol RTyCon RTyVar RReft -> ([Symbol], [Symbol])
collectSpecTypeBinders RTypeBV Symbol Symbol RTyCon RTyVar RReft
querySpecType



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

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

  rename ExprBV Symbol Symbol
e = Maybe SrcSpan -> [Char] -> ExprBV Symbol Symbol
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic
    Maybe SrcSpan
forall a. Maybe a
Nothing
    ([Char]
"renameBinderCoerc: Not sure how to handle the expression " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ExprBV Symbol Symbol -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp ExprBV Symbol Symbol
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 (F.FNatNum Integer
n)      = Integer -> Sort
F.FNatNum Integer
n
  rename Sort
F.FFrac            = Sort
F.FFrac
  rename (   F.FObj Symbol
s     ) = Symbol -> Sort
F.FObj (Symbol -> Symbol
f Symbol
s)
  rename t' :: Sort
t'@(F.FVar Int
_     ) = Sort
t'
  rename (   F.FFunc Sort
t0 Sort
t1) = Sort -> Sort -> Sort
F.FFunc (Sort -> Sort
rename Sort
t0) (Sort -> Sort
rename Sort
t1)
  rename (   F.FAbs  Int
x  Sort
t') = Int -> Sort -> Sort
F.FAbs Int
x (Sort -> Sort
rename Sort
t')
  rename t' :: Sort
t'@(F.FTC FTycon
_      ) = Sort
t'
  rename (   F.FApp Sort
t0 Sort
t1 ) = Sort -> Sort -> Sort
F.FApp (Sort -> Sort
rename Sort
t0) (Sort -> Sort
rename Sort
t1)


-- | Embed fixpoint expressions into parsed haskell expressions.
--   It allows us to bypass the GHC parser and use arbitrary symbols
--   for identifiers (compared to using the string API)
fixExprToHsExpr :: S.HashSet F.Symbol -> F.Expr -> LHsExpr GhcPs
fixExprToHsExpr :: HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
_ (F.ECon Constant
c) = Constant -> LHsExpr (GhcPass 'Parsed)
constantToHsExpr Constant
c
fixExprToHsExpr HashSet Symbol
env (F.EVar Symbol
x)
  | Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Name -> [Char]
forall a. Show a => a -> [Char]
show '[]) =  [Char] -> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall a. Outputable a => [Char] -> a -> a
GM.notracePpr [Char]
"Empty" (LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed))
-> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall a b. (a -> b) -> a -> b
$ IdP (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
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
== [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Name -> [Char]
forall a. Show a => a -> [Char]
show '(:)) = [Char] -> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall a. Outputable a => [Char] -> a -> a
GM.notracePpr [Char]
"Cons" (LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed))
-> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall a b. (a -> b) -> a -> b
$ IdP (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
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 (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall a. Outputable a => [Char] -> a -> a
GM.notracePpr [Char]
"Var" (LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed))
-> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall a b. (a -> b) -> a -> b
$ IdP (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
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 ExprBV Symbol Symbol
e0 ExprBV Symbol Symbol
e1) =
  LHsExpr (GhcPass 'Parsed)
-> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
e0) (HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
e1)
fixExprToHsExpr HashSet Symbol
env (F.ENeg ExprBV Symbol Symbol
e) =
  LHsExpr (GhcPass 'Parsed)
-> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (IdP (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (Name -> RdrName
nameRdrName Name
negateName)) (HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
e)

fixExprToHsExpr HashSet Symbol
env (F.EBin Bop
bop ExprBV Symbol Symbol
e0 ExprBV Symbol Symbol
e1) = LHsExpr (GhcPass 'Parsed)
-> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
  (LHsExpr (GhcPass 'Parsed)
-> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (Bop -> LHsExpr (GhcPass 'Parsed)
bopToHsExpr Bop
bop) (HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
e0))
  (HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
e1)
fixExprToHsExpr HashSet Symbol
env (F.EIte ExprBV Symbol Symbol
p ExprBV Symbol Symbol
e0 ExprBV Symbol Symbol
e1) = LHsExpr (GhcPass 'Parsed)
-> LHsExpr (GhcPass 'Parsed)
-> LHsExpr (GhcPass 'Parsed)
-> LHsExpr (GhcPass 'Parsed)
nlHsIf (HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
p)
                                              (HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
e0)
                                              (HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
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 ExprBV Symbol Symbol
e0 Sort
_    ) = HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
e0
-- fixExprToHsExpr env (F.PAnd []      ) = nlHsVar true_RDR
fixExprToHsExpr HashSet Symbol
_ (F.PAnd []      ) = IdP (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar IdP (GhcPass 'Parsed)
RdrName
true_RDR
fixExprToHsExpr HashSet Symbol
env (F.PAnd (ExprBV Symbol Symbol
e : [ExprBV Symbol Symbol]
es)) = (ExprBV Symbol Symbol
 -> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed))
 -> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed)))
-> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed))
-> [ExprBV Symbol Symbol]
-> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed))
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
L.foldr ExprBV Symbol Symbol
-> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed))
-> LHsExpr (GhcPass 'Parsed)
ExprBV Symbol Symbol
-> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed))
-> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed))
f (HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
e) [ExprBV Symbol Symbol]
es
 where
  f :: ExprBV Symbol Symbol
-> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed))
-> LHsExpr (GhcPass 'Parsed)
f ExprBV Symbol Symbol
x GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed))
acc = LHsExpr (GhcPass 'Parsed)
-> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (LHsExpr (GhcPass 'Parsed)
-> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (IdP (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar IdP (GhcPass 'Parsed)
RdrName
and_RDR) (HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
x)) LHsExpr (GhcPass 'Parsed)
GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed))
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 [ExprBV Symbol Symbol]
es) = LHsExpr (GhcPass 'Parsed)
-> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
  (IdP (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (Module -> FastString -> RdrName
varQual_RDR Module
foldableModule ([Char] -> FastString
fsLit [Char]
"or")))
  ([LHsExpr (GhcPass 'Parsed)] -> LHsExpr (GhcPass 'Parsed)
nlList ([LHsExpr (GhcPass 'Parsed)] -> LHsExpr (GhcPass 'Parsed))
-> [LHsExpr (GhcPass 'Parsed)] -> LHsExpr (GhcPass 'Parsed)
forall a b. (a -> b) -> a -> b
$ HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env (ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed))
-> [ExprBV Symbol Symbol] -> [LHsExpr (GhcPass 'Parsed)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprBV Symbol Symbol]
es)
fixExprToHsExpr HashSet Symbol
env (F.PIff ExprBV Symbol Symbol
e0 ExprBV Symbol Symbol
e1) = LHsExpr (GhcPass 'Parsed)
-> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
  (LHsExpr (GhcPass 'Parsed)
-> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (IdP (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
"<=>"))) (HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
e0)
  )
  (HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
e1)
fixExprToHsExpr HashSet Symbol
env (F.PNot ExprBV Symbol Symbol
e) =
  LHsExpr (GhcPass 'Parsed)
-> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (IdP (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar IdP (GhcPass 'Parsed)
RdrName
not_RDR) (HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
e)
fixExprToHsExpr HashSet Symbol
env (F.PAtom Brel
brel ExprBV Symbol Symbol
e0 ExprBV Symbol Symbol
e1) = LHsExpr (GhcPass 'Parsed)
-> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
  (LHsExpr (GhcPass 'Parsed)
-> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (Brel -> LHsExpr (GhcPass 'Parsed)
brelToHsExpr Brel
brel) (HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
e0))
  (HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
e1)
fixExprToHsExpr HashSet Symbol
env (F.PImp ExprBV Symbol Symbol
e0 ExprBV Symbol Symbol
e1) = LHsExpr (GhcPass 'Parsed)
-> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
  (LHsExpr (GhcPass 'Parsed)
-> LHsExpr (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (IdP (GhcPass 'Parsed) -> LHsExpr (GhcPass 'Parsed)
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
"==>"))) (HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
e0)
  )
  (HashSet Symbol -> ExprBV Symbol Symbol -> LHsExpr (GhcPass 'Parsed)
fixExprToHsExpr HashSet Symbol
env ExprBV Symbol Symbol
e1)

fixExprToHsExpr HashSet Symbol
_ ExprBV Symbol Symbol
e =
  Maybe SrcSpan
-> [Char] -> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed))
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]
++ ExprBV Symbol Symbol -> [Char]
forall a. Show a => a -> [Char]
show ExprBV Symbol Symbol
e)

constantToHsExpr :: F.Constant -> LHsExpr GhcPs
-- constantToHsExpr (F.I c) = noLoc (HsLit NoExt (HsInt NoExt (mkIntegralLit c)))
constantToHsExpr :: Constant -> LHsExpr (GhcPass 'Parsed)
constantToHsExpr (F.I Integer
i) =
  HsExpr (GhcPass 'Parsed)
-> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed))
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (HsExpr (GhcPass 'Parsed)
 -> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed)))
-> HsExpr (GhcPass 'Parsed)
-> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed))
forall a b. (a -> b) -> a -> b
$ HsOverLit (GhcPass 'Parsed) -> HsExpr (GhcPass 'Parsed)
mkHsOverLit (IntegralLit -> HsOverLit (GhcPass 'Parsed)
mkHsIntegral (Integer -> IntegralLit
forall a. Integral a => a -> IntegralLit
mkIntegralLit Integer
i))
constantToHsExpr (F.R Double
d) =
  HsExpr (GhcPass 'Parsed)
-> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed))
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (HsExpr (GhcPass 'Parsed)
 -> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed)))
-> HsExpr (GhcPass 'Parsed)
-> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed))
forall a b. (a -> b) -> a -> b
$ HsOverLit (GhcPass 'Parsed) -> HsExpr (GhcPass 'Parsed)
mkHsOverLit (FractionalLit -> HsOverLit (GhcPass 'Parsed)
mkHsFractional (Rational -> FractionalLit
mkTHFractionalLit (Double -> Rational
forall a. Real a => a -> Rational
toRational Double
d)))
constantToHsExpr Constant
_ =
  Maybe SrcSpan
-> [Char] -> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed))
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 (GhcPass 'Parsed)
bopToHsExpr Bop
bop = HsExpr (GhcPass 'Parsed)
-> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Parsed))
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (XVar (GhcPass 'Parsed)
-> LIdOccP (GhcPass 'Parsed) -> HsExpr (GhcPass 'Parsed)
forall p. XVar p -> LIdOccP p -> HsExpr p
HsVar XVar (GhcPass 'Parsed)
NoExtField
Ghc.noExtField (RdrName -> GenLocated SrcSpanAnnN RdrName
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (Bop -> RdrName
f Bop
bop)))
 where
  f :: Bop -> RdrName
f Bop
F.Plus   = RdrName
plus_RDR
  f Bop
F.Minus  = RdrName
minus_RDR
  f Bop
F.Times  = RdrName
times_RDR
  f Bop
F.Div    = FastString -> RdrName
mkVarUnqual ([Char] -> FastString
fsLit [Char]
"/")
  f Bop
F.Mod    = FastString -> RdrName
GM.prependGHCRealQual ([Char] -> FastString
fsLit [Char]
"mod")
  f Bop
F.RTimes = RdrName
times_RDR
  f Bop
F.RDiv   = FastString -> RdrName
GM.prependGHCRealQual ([Char] -> FastString
fsLit [Char]
"/")

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

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


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


-- don't use this function...
symbolToRdrName :: S.HashSet F.Symbol -> F.Symbol -> RdrName
symbolToRdrName :: HashSet Symbol -> Symbol -> RdrName
symbolToRdrName HashSet Symbol
env Symbol
x
  | Symbol -> Bool
F.isNonSymbol Symbol
modName = NameSpace -> FastString -> RdrName
mkUnqual NameSpace
ns ([Char] -> FastString
mkFastString (Symbol -> [Char]
F.symbolString Symbol
s))
  | Bool
otherwise = NameSpace -> (FastString, FastString) -> RdrName
mkQual
    NameSpace
ns
    ([Char] -> FastString
mkFastString (Symbol -> [Char]
F.symbolString Symbol
modName), [Char] -> FastString
mkFastString (Symbol -> [Char]
F.symbolString Symbol
s))
 where
  (Symbol
modName, Symbol
s) = Symbol -> (Symbol, Symbol)
GM.splitModuleName Symbol
x
  ns :: NameSpace
ns | Bool -> Bool
not (Symbol -> HashSet Symbol -> Bool
forall a. 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 :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> LHsType (GhcPass 'Parsed)
specTypeToLHsType = \case
    RVar (RTV Var
tv) RReft
_ -> PromotionFlag -> IdP (GhcPass 'Parsed) -> LHsType (GhcPass 'Parsed)
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 (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
tv))
    RFun Symbol
_ RFInfo
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout RReft
_
      | RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin -> HsType (GhcPass 'Parsed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Parsed))
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (HsType (GhcPass 'Parsed)
 -> GenLocated SrcSpanAnnA (HsType (GhcPass 'Parsed)))
-> HsType (GhcPass 'Parsed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Parsed))
forall a b. (a -> b) -> a -> b
$ XQualTy (GhcPass 'Parsed)
-> LHsContext (GhcPass 'Parsed)
-> LHsType (GhcPass 'Parsed)
-> HsType (GhcPass 'Parsed)
forall pass.
XQualTy pass -> LHsContext pass -> LHsType pass -> HsType pass
HsQualTy XQualTy (GhcPass 'Parsed)
NoExtField
Ghc.noExtField ([LHsType (GhcPass 'Parsed)]
-> GenLocated SrcSpanAnnC [LHsType (GhcPass 'Parsed)]
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA [RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> LHsType (GhcPass 'Parsed)
specTypeToLHsType RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin]) (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> LHsType (GhcPass 'Parsed)
specTypeToLHsType RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout)
      | Bool
otherwise       -> LHsType (GhcPass 'Parsed)
-> LHsType (GhcPass 'Parsed) -> LHsType (GhcPass 'Parsed)
forall (p :: Pass).
IsPass p =>
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsFunTy (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> LHsType (GhcPass 'Parsed)
specTypeToLHsType RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin) (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> LHsType (GhcPass 'Parsed)
specTypeToLHsType RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout)
    RAllT (RTVUBV Symbol Symbol RTyCon RTyVar -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value -> (RTV Var
tv)) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RReft
_ -> HsType (GhcPass 'Parsed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Parsed))
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (HsType (GhcPass 'Parsed)
 -> GenLocated SrcSpanAnnA (HsType (GhcPass 'Parsed)))
-> HsType (GhcPass 'Parsed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Parsed))
forall a b. (a -> b) -> a -> b
$ XForAllTy (GhcPass 'Parsed)
-> HsForAllTelescope (GhcPass 'Parsed)
-> LHsType (GhcPass 'Parsed)
-> HsType (GhcPass 'Parsed)
forall pass.
XForAllTy pass
-> HsForAllTelescope pass -> LHsType pass -> HsType pass
HsForAllTy
      XForAllTy (GhcPass 'Parsed)
NoExtField
Ghc.noExtField
      (EpAnn (TokForall, EpToken ".")
-> [LHsTyVarBndr Specificity (GhcPass 'Parsed)]
-> HsForAllTelescope (GhcPass 'Parsed)
forall (p :: Pass).
EpAnn (TokForall, EpToken ".")
-> [LHsTyVarBndr Specificity (GhcPass p)]
-> HsForAllTelescope (GhcPass p)
mkHsForAllInvisTele EpAnn (TokForall, EpToken ".")
forall a. NoAnn a => a
noAnn
        [ HsTyVarBndr Specificity (GhcPass 'Parsed)
-> GenLocated
     SrcSpanAnnA (HsTyVarBndr Specificity (GhcPass 'Parsed))
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (HsTyVarBndr Specificity (GhcPass 'Parsed)
 -> GenLocated
      SrcSpanAnnA (HsTyVarBndr Specificity (GhcPass 'Parsed)))
-> HsTyVarBndr Specificity (GhcPass 'Parsed)
-> GenLocated
     SrcSpanAnnA (HsTyVarBndr Specificity (GhcPass 'Parsed))
forall a b. (a -> b) -> a -> b
$
            XTyVarBndr (GhcPass 'Parsed)
-> Specificity
-> HsBndrVar (GhcPass 'Parsed)
-> HsBndrKind (GhcPass 'Parsed)
-> HsTyVarBndr Specificity (GhcPass 'Parsed)
forall flag pass.
XTyVarBndr pass
-> flag
-> HsBndrVar pass
-> HsBndrKind pass
-> HsTyVarBndr flag pass
Ghc.HsTvb
              XTyVarBndr (GhcPass 'Parsed)
forall a. NoAnn a => a
noAnn
              Specificity
Ghc.SpecifiedSpec
              (XBndrVar (GhcPass 'Parsed)
-> LIdP (GhcPass 'Parsed) -> HsBndrVar (GhcPass 'Parsed)
forall pass. XBndrVar pass -> LIdP pass -> HsBndrVar pass
Ghc.HsBndrVar NoExtField
XBndrVar (GhcPass 'Parsed)
Ghc.noExtField (RdrName -> GenLocated SrcSpanAnnN RdrName
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (RdrName -> GenLocated SrcSpanAnnN RdrName)
-> RdrName -> GenLocated SrcSpanAnnN RdrName
forall a b. (a -> b) -> a -> b
$ NameSpace -> Symbol -> RdrName
symbolToRdrNameNs NameSpace
tvName (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
tv)))
              (XBndrNoKind (GhcPass 'Parsed) -> HsBndrKind (GhcPass 'Parsed)
forall pass. XBndrNoKind pass -> HsBndrKind pass
Ghc.HsBndrNoKind NoExtField
XBndrNoKind (GhcPass 'Parsed)
Ghc.noExtField)
        ]
      )
      (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> LHsType (GhcPass 'Parsed)
specTypeToLHsType RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
    RAllP PVUBV Symbol Symbol RTyCon RTyVar
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> LHsType (GhcPass 'Parsed)
specTypeToLHsType RTypeBV Symbol Symbol RTyCon RTyVar RReft
ty
    RApp RTyCon { rtc_tc :: RTyCon -> TyCon
rtc_tc = TyCon
tc } [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
_ RReft
_ -> IdP (GhcPass 'Parsed)
-> [LHsType (GhcPass 'Parsed)] -> LHsType (GhcPass 'Parsed)
mkHsTyConApp
      (TyCon -> RdrName
forall thing. NamedThing thing => thing -> RdrName
getRdrName TyCon
tc)
      [ RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> LHsType (GhcPass 'Parsed)
specTypeToLHsType RTypeBV Symbol Symbol RTyCon RTyVar RReft
t | RTypeBV Symbol Symbol RTyCon RTyVar RReft
t <- [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts, RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Bool
forall v c tv r. RTypeV v c tv r -> Bool
notExprArg RTypeBV Symbol Symbol RTyCon RTyVar RReft
t ]
    RAllE Symbol
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout -> LHsType (GhcPass 'Parsed)
-> LHsType (GhcPass 'Parsed) -> LHsType (GhcPass 'Parsed)
forall (p :: Pass).
IsPass p =>
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsFunTy (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> LHsType (GhcPass 'Parsed)
specTypeToLHsType RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin) (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> LHsType (GhcPass 'Parsed)
specTypeToLHsType RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout)
    REx Symbol
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout -> LHsType (GhcPass 'Parsed)
-> LHsType (GhcPass 'Parsed) -> LHsType (GhcPass 'Parsed)
forall (p :: Pass).
IsPass p =>
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsFunTy (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> LHsType (GhcPass 'Parsed)
specTypeToLHsType RTypeBV Symbol Symbol RTyCon RTyVar RReft
tin) (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> LHsType (GhcPass 'Parsed)
specTypeToLHsType RTypeBV Symbol Symbol RTyCon RTyVar RReft
tout)
    RAppTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
_ (RExprArg Located (ExprBV Symbol Symbol)
_) RReft
_ ->
      Maybe SrcSpan
-> [Char] -> GenLocated SrcSpanAnnA (HsType (GhcPass 'Parsed))
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"RExprArg should not appear here"
    RAppTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RTypeBV Symbol Symbol RTyCon RTyVar RReft
t' RReft
_ -> LHsType (GhcPass 'Parsed)
-> LHsType (GhcPass 'Parsed) -> LHsType (GhcPass 'Parsed)
forall (p :: Pass).
IsPass p =>
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsFunTy (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> LHsType (GhcPass 'Parsed)
specTypeToLHsType RTypeBV Symbol Symbol RTyCon RTyVar RReft
t) (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> LHsType (GhcPass 'Parsed)
specTypeToLHsType RTypeBV Symbol Symbol RTyCon RTyVar RReft
t')
    RRTy [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
_ RReft
_ Oblig
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> LHsType (GhcPass 'Parsed)
specTypeToLHsType RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
    RHole RReft
_ -> HsType (GhcPass 'Parsed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Parsed))
forall e a. HasAnnotation e => a -> GenLocated e a
noLocA (HsType (GhcPass 'Parsed)
 -> GenLocated SrcSpanAnnA (HsType (GhcPass 'Parsed)))
-> HsType (GhcPass 'Parsed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Parsed))
forall a b. (a -> b) -> a -> b
$ XWildCardTy (GhcPass 'Parsed) -> HsType (GhcPass 'Parsed)
forall pass. XWildCardTy pass -> HsType pass
HsWildCardTy XWildCardTy (GhcPass 'Parsed)
forall a. NoAnn a => a
Ghc.noAnn
    RExprArg Located (ExprBV Symbol Symbol)
_ ->
      Maybe SrcSpan
-> [Char] -> GenLocated SrcSpanAnnA (HsType (GhcPass 'Parsed))
forall a. Maybe SrcSpan -> [Char] -> a
todo Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Oops, specTypeToLHsType doesn't know how to handle RExprArg"