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

{-# OPTIONS_GHC -Wno-orphans #-}

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

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

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

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

import qualified Language.Fixpoint.Types       as F
-- import           Control.Arrow
import           Liquid.GHC.API hiding (panic, varName)
import qualified Language.Haskell.Liquid.GHC.Misc
                                               as GM
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Types.RefType
                                                ( ofType )
import qualified Data.List                     as L
import qualified Data.HashMap.Strict           as M
import qualified Data.HashSet                  as S
import           Control.Monad.Free
#if MIN_VERSION_recursion_schemes(5,2,0)
import           Data.Fix                      hiding (hylo)
import           Data.Functor.Foldable         hiding (Fix)
#else
import           Data.Functor.Foldable
#endif

import           Data.Char                      ( isUpper )
import           GHC.Types.Name.Occurrence
import qualified Liquid.GHC.API as Ghc
                                                (noExtField)
import           Data.Default                   ( def )
import qualified Data.Maybe                    as Mb

-- TODO: make elaboration monadic so typeclass names are unified to something
-- that is generated in advance. This can greatly simplify the implementation
-- of elaboration

-- the substitution code is meant to inline dictionary functions
-- but does not seem to work
-- lookupIdSubstAll :: O.SDoc -> M.HashMap Id CoreExpr -> Id -> CoreExpr
-- lookupIdSubstAll doc env v | Just e <- M.lookup v env = e
--                            | otherwise                = Var v
--         -- Vital! See Note [Extending the Subst]
--   -- | otherwise = WARN( True, text "CoreSubst.lookupIdSubst" <+> doc <+> ppr v
--   --                           $$ ppr in_scope)

-- substExprAll :: O.SDoc -> M.HashMap Id CoreExpr -> CoreExpr -> CoreExpr
-- substExprAll doc subst orig_expr = subst_expr_all doc subst orig_expr


-- subst_expr_all :: O.SDoc -> M.HashMap Id CoreExpr -> CoreExpr -> CoreExpr
-- subst_expr_all doc subst expr = go expr
--  where
--   go (Var v) = lookupIdSubstAll (doc O.$$ O.text "subst_expr_all") subst v
--   go (Type     ty      ) = Type ty
--   go (Coercion co      ) = Coercion co
--   go (Lit      lit     ) = Lit lit
--   go (App  fun     arg ) = App (go fun) (go arg)
--   go (Tick tickish e   ) = Tick tickish (go e)
--   go (Cast e       co  ) = Cast (go e) co
--      -- Do not optimise even identity coercions
--      -- Reason: substitution applies to the LHS of RULES, and
--      --         if you "optimise" an identity coercion, you may
--      --         lose a binder. We optimise the LHS of rules at
--      --         construction time

--   go (Lam  bndr    body) = Lam bndr (subst_expr_all doc subst body)

--   go (Let  bind    body) = Let (mapBnd go bind) (subst_expr_all doc subst body)

--   go (Case scrut bndr ty alts) =
--     Case (go scrut) bndr ty (map (go_alt subst) alts)

--   go_alt subst (con, bndrs, rhs) = (con, bndrs, subst_expr_all doc subst rhs)


-- mapBnd :: (Expr b -> Expr b) -> Bind b -> Bind b
-- mapBnd f (NonRec b e) = NonRec b (f e)
-- mapBnd f (Rec bs    ) = Rec (map (second f) bs)

-- -- substLet :: CoreExpr -> CoreExpr
-- -- substLet (Lam b body) = Lam b (substLet body)
-- -- substLet (Let b body)
-- --   | NonRec x e <- b = substLet
-- --     (substExprAll O.empty (extendIdSubst emptySubst x e) body)
-- --   | otherwise = Let b (substLet body)
-- -- substLet e = e


-- buildDictSubst :: CoreProgram -> M.HashMap Id CoreExpr
-- buildDictSubst = cata f
--  where
--   f Nil = M.empty
--   f (Cons b s) | NonRec x e <- b, isDFunId x -- || isDictonaryId x
--                                              = M.insert x e s
--                | otherwise                   = s

-- buildSimplifier :: CoreProgram -> CoreExpr -> TcRn CoreExpr
-- buildSimplifier cbs e = pure e-- do
 --  df <- getDynFlags
 --  liftIO $ simplifyExpr (df `gopt_set` Opt_SuppressUnfoldings) e'
 -- where
 --  -- fvs = fmap (\x -> (x, getUnique x, isLocalId x))  (freeVars mempty e)
 --  dictSubst = buildDictSubst cbs
 --  e'        = substExprAll O.empty dictSubst e


-- | Base functor of RType
data RTypeF c tv r f
  = RVarF {
      forall c tv r f. RTypeF c tv r f -> tv
rtf_var    :: !tv
    , forall c tv r f. RTypeF c tv r f -> r
rtf_reft   :: !r
    }

  | RFunF  {
      forall c tv r f. RTypeF c tv r f -> Symbol
rtf_bind   :: !F.Symbol
    , forall c tv r f. RTypeF c tv r f -> RFInfo
rtf_rinfo  :: !RFInfo
    , forall c tv r f. RTypeF c tv r f -> f
rtf_in     :: !f
    , forall c tv r f. RTypeF c tv r f -> f
rtf_out    :: !f
    , rtf_reft   :: !r
    }
  | RAllTF {
      forall c tv r f. RTypeF c tv r f -> RTVU c tv
rtf_tvbind :: !(RTVU c tv) -- RTVar tv (RType c tv ()))
    , forall c tv r f. RTypeF c tv r f -> f
rtf_ty     :: !f
    , forall c tv r f. RTypeF c tv r f -> r
rtf_ref    :: !r
    }

  -- | "forall x y <z :: Nat, w :: Int> . TYPE"
  --               ^^^^^^^^^^^^^^^^^^^ (rtf_pvbind)
  | RAllPF {
      forall c tv r f. RTypeF c tv r f -> PVU c tv
rtf_pvbind :: !(PVU c tv)  -- ar (RType c tv ()))
    , rtf_ty     :: !f
    }

  -- | For example, in [a]<{\h -> v > h}>, we apply (via `RApp`)
  --   * the `RProp`  denoted by `{\h -> v > h}` to
  --   * the `RTyCon` denoted by `[]`.
  | RAppF  {
      forall c tv r f. RTypeF c tv r f -> c
rtf_tycon  :: !c
    , forall c tv r f. RTypeF c tv r f -> [f]
rtf_args   :: ![f]
    , forall c tv r f. RTypeF c tv r f -> [RTPropF c tv f]
rtf_pargs  :: ![RTPropF c tv f]
    , rtf_reft   :: !r
    }

  | RAllEF {
      rtf_bind   :: !F.Symbol
    , forall c tv r f. RTypeF c tv r f -> f
rtf_allarg :: !f
    , rtf_ty     :: !f
    }

  | RExF {
      rtf_bind   :: !F.Symbol
    , forall c tv r f. RTypeF c tv r f -> f
rtf_exarg  :: !f
    , rtf_ty     :: !f
    }

  | RExprArgF (F.Located F.Expr)

  | RAppTyF{
      forall c tv r f. RTypeF c tv r f -> f
rtf_arg   :: !f
    , forall c tv r f. RTypeF c tv r f -> f
rtf_res   :: !f
    , rtf_reft  :: !r
    }

  | RRTyF  {
      forall c tv r f. RTypeF c tv r f -> [(Symbol, f)]
rtf_env   :: ![(F.Symbol, f)]
    , rtf_ref   :: !r
    , forall c tv r f. RTypeF c tv r f -> Oblig
rtf_obl   :: !Oblig
    , rtf_ty    :: !f
    }

  | RHoleF r
  deriving (forall a b. a -> 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
<$ :: forall a b. a -> RTypeF c tv r b -> RTypeF c tv r a
$c<$ :: forall c tv r a b. a -> RTypeF c tv r b -> RTypeF c tv r a
fmap :: forall a b. (a -> b) -> RTypeF c tv r a -> RTypeF c tv r b
$cfmap :: forall c tv r a b. (a -> b) -> RTypeF c tv r a -> RTypeF c tv r b
Functor)

-- It's probably ok to treat (RType c tv ()) as a leaf..
type RTPropF c tv f = Ref (RType c tv ()) f


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

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

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

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

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


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

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

-- A one-way function. Kind of like injecting something into Maybe
specTypeToPartial :: forall a . SpecType -> SpecTypeF (Free SpecTypeF a)
specTypeToPartial :: forall a.
RType RTyCon RTyVar RReft
-> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
specTypeToPartial = forall (f :: * -> *) b a.
Functor f =>
(f b -> b) -> (a -> f a) -> a -> b
hylo (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap) forall t. Recursive t => t -> Base t t
project

-- probably should return spectype instead..
plugType :: SpecType -> PartialSpecType -> SpecType
plugType :: RType RTyCon RTyVar RReft
-> PartialSpecType -> RType RTyCon RTyVar RReft
plugType RType RTyCon RTyVar RReft
t = forall s t. (Recursive s, Corecursive t, Base s ~ Base t) => s -> t
refix forall b c a. (b -> c) -> (a -> b) -> a -> c
. PartialSpecType -> Fix (RTypeF RTyCon RTyVar RReft)
f
 where
  f :: PartialSpecType -> Fix (RTypeF RTyCon RTyVar RReft)
f = forall (f :: * -> *) b a.
Functor f =>
(f b -> b) -> (a -> f a) -> a -> b
hylo forall (f :: * -> *). f (Fix f) -> Fix f
Fix forall a b. (a -> b) -> a -> b
$ \case
    Pure ()
_   -> forall a.
RType RTyCon RTyVar RReft
-> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
specTypeToPartial RType RTyCon RTyVar RReft
t
    Free RTypeF RTyCon RTyVar RReft PartialSpecType
res -> RTypeF RTyCon RTyVar RReft PartialSpecType
res

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

-- | returns (lambda binders, forall binders)
collectSpecTypeBinders :: SpecType -> ([F.Symbol], [F.Symbol])
collectSpecTypeBinders :: RType RTyCon RTyVar RReft -> ([Symbol], [Symbol])
collectSpecTypeBinders = forall t a. Recursive t => (Base t (t, a) -> a) -> t -> a
para forall a b. (a -> b) -> a -> b
$ \case
  RFunF Symbol
bind RFInfo
_ (RType RTyCon RTyVar RReft
tin, ([Symbol], [Symbol])
_) (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs')) RReft
_ | forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType RTyCon RTyVar RReft
tin -> ([Symbol]
bs, [Symbol]
abs')
                                       | Bool
otherwise       -> (Symbol
bind forall a. a -> [a] -> [a]
: [Symbol]
bs, [Symbol]
abs')
  RAllEF Symbol
b (RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
_ (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs'))  -> (Symbol
b forall a. a -> [a] -> [a]
: [Symbol]
bs, [Symbol]
abs')
  RAllTF (RTVar (RTV TyVar
ab) RTVInfo (RType RTyCon RTyVar ())
_) (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs')) RReft
_ -> ([Symbol]
bs, forall a. Symbolic a => a -> Symbol
F.symbol TyVar
ab forall a. a -> [a] -> [a]
: [Symbol]
abs')
  RExF Symbol
b (RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
_ (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs'))    -> (Symbol
b forall a. a -> [a] -> [a]
: [Symbol]
bs, [Symbol]
abs')
  RAppTyF (RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
_ (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs')) RReft
_ -> ([Symbol]
bs, [Symbol]
abs')
  RRTyF [(Symbol, (RType RTyCon RTyVar RReft, ([Symbol], [Symbol])))]
_ RReft
_ Oblig
_ (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs')) -> ([Symbol]
bs, [Symbol]
abs')
  Base
  (RType RTyCon RTyVar RReft)
  (RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
_                          -> ([], [])

-- really should be fused with collectBinders. However, we need the binders
-- to correctly convert fixpoint expressions to ghc expressions because of
-- namespace related issues (whether the symbol denotes a varName or a datacon)
buildHsExpr :: LHsExpr GhcPs -> SpecType -> LHsExpr GhcPs
buildHsExpr :: LHsExpr GhcPs -> RType RTyCon RTyVar RReft -> LHsExpr GhcPs
buildHsExpr LHsExpr GhcPs
result = forall t a. Recursive t => (Base t (t, a) -> a) -> t -> a
para forall a b. (a -> b) -> a -> b
$ \case
  RFunF Symbol
bind RFInfo
_ (RType RTyCon RTyVar RReft
tin, GenLocated SrcSpanAnnA (HsExpr GhcPs)
_) (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res) RReft
_
    | forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType RTyCon RTyVar RReft
tin -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
    | Bool
otherwise       -> forall (p :: Pass).
(IsPass p, XMG (GhcPass p) (LHsExpr (GhcPass p)) ~ NoExtField) =>
[LPat (GhcPass p)] -> LHsExpr (GhcPass p) -> LHsExpr (GhcPass p)
mkHsLam [forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LPat (GhcPass p)
nlVarPat (Symbol -> RdrName
varSymbolToRdrName Symbol
bind)] GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
  RAllEF  Symbol
_ (RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsExpr GhcPs))
_        (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res) -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
  RAllTF  RTVar RTyVar (RType RTyCon RTyVar ())
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res) RReft
_        -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
  RExF    Symbol
_ (RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsExpr GhcPs))
_        (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res) -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
  RAppTyF (RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsExpr GhcPs))
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res) RReft
_        -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
  RRTyF [(Symbol,
  (RType RTyCon RTyVar RReft,
   GenLocated SrcSpanAnnA (HsExpr GhcPs)))]
_ RReft
_ Oblig
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res)        -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
  Base
  (RType RTyCon RTyVar RReft)
  (RType RTyCon RTyVar RReft, LHsExpr GhcPs)
_                           -> LHsExpr GhcPs
result



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

elaborateSpecType
  :: (CoreExpr -> F.Expr)
  -> (CoreExpr -> TcRn CoreExpr)
  -> SpecType
  -> TcRn SpecType
elaborateSpecType :: (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft)
elaborateSpecType CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplifier RType RTyCon RTyVar RReft
t = forall a. TcM a -> TcM a
GM.withWiredIn forall a b. (a -> b) -> a -> b
$ do
  (RType RTyCon RTyVar RReft
t', [Symbol]
xs) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' (forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplifier RType RTyCon RTyVar RReft
t
  case [Symbol]
xs of
    Symbol
_ : [Symbol]
_ -> forall a. Maybe SrcSpan -> [Char] -> a
panic
      forall a. Maybe a
Nothing
      [Char]
"elaborateSpecType: invariant broken. substitution list for dictionary is not completely consumed"
    [Symbol]
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure RType RTyCon RTyVar RReft
t'

elaborateSpecType'
  :: PartialSpecType
  -> (CoreExpr -> F.Expr) -- core to logic
  -> (CoreExpr -> TcRn CoreExpr)
  -> SpecType
  -> TcRn (SpecType, [F.Symbol]) -- binders for dictionaries
                   -- should have returned Maybe [F.Symbol]
elaborateSpecType' :: PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
t =
  case forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"elaborateSpecType'" RType RTyCon RTyVar RReft
t of
    RVar (RTV TyVar
tv) (MkUReft reft :: Reft
reft@(F.Reft (Symbol
vv, Expr
_oldE)) Predicate
p) -> do
      forall a.
PPrint a =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft
        (Reft
reft, RType RTyCon RTyVar RReft
t)
        (forall (f :: * -> *) a. Applicative f => a -> f a
pure (RType RTyCon RTyVar RReft
t, []))
        (\[Symbol]
bs' Expr
ee -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall c tv r. tv -> r -> RType c tv r
RVar (TyVar -> RTyVar
RTV TyVar
tv) (forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
ee)) Predicate
p), [Symbol]
bs'))
        -- YL : Fix
    RFun  Symbol
bind RFInfo
i RType RTyCon RTyVar RReft
tin RType RTyCon RTyVar RReft
tout ureft :: RReft
ureft@(MkUReft reft :: Reft
reft@(F.Reft (Symbol
vv, Expr
_oldE)) Predicate
p) -> do
      -- the reft is never actually used by the child
      -- maybe i should enforce this information at the type level
      let partialFunTp :: PartialSpecType
partialFunTp =
            forall (f :: * -> *) a. f (Free f a) -> Free f a
Free (forall c tv r f. Symbol -> RFInfo -> f -> f -> r -> RTypeF c tv r f
RFunF Symbol
bind RFInfo
i (forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap forall a b. (a -> b) -> a -> b
$ forall a.
RType RTyCon RTyVar RReft
-> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
specTypeToPartial RType RTyCon RTyVar RReft
tin) (forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) RReft
ureft) :: PartialSpecType
          partialTp' :: PartialSpecType
partialTp' = PartialSpecType
partialTp forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> PartialSpecType
partialFunTp :: PartialSpecType
      (RType RTyCon RTyVar RReft
eTin , [Symbol]
bs ) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
tin
      (RType RTyCon RTyVar RReft
eTout, [Symbol]
bs') <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp' CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
tout
      let buildRFunContTrivial :: TcRn (RType RTyCon RTyVar RReft, [Symbol])
buildRFunContTrivial
            | forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType RTyCon RTyVar RReft
tin, Symbol
dictBinder : [Symbol]
bs0' <- [Symbol]
bs' = do
              let (RType RTyCon RTyVar RReft
eToutRenamed, [Symbol]
canonicalBinders) =
                    forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eTout, [Symbol]
bs0')
              forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"RFunTrivial0"
                  forall a b. (a -> b) -> a -> b
$ forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
dictBinder RFInfo
i RType RTyCon RTyVar RReft
eTin RType RTyCon RTyVar RReft
eToutRenamed RReft
ureft
                , [Symbol]
canonicalBinders
                )
            | Bool
otherwise = do
              let (RType RTyCon RTyVar RReft
eToutRenamed, [Symbol]
canonicalBinders) =
                    forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eTout, [Symbol]
bs')
              forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"RFunTrivial1" forall a b. (a -> b) -> a -> b
$ forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
bind RFInfo
i RType RTyCon RTyVar RReft
eTin RType RTyCon RTyVar RReft
eToutRenamed RReft
ureft
                , [Symbol]
canonicalBinders
                )
          buildRFunCont :: [Symbol] -> Expr -> TcRn (RType RTyCon RTyVar RReft, [Symbol])
buildRFunCont [Symbol]
bs'' Expr
ee
            | forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType RTyCon RTyVar RReft
tin, Symbol
dictBinder : [Symbol]
bs0' <- [Symbol]
bs' = do
              let (RType RTyCon RTyVar RReft
eToutRenamed, [Symbol]
canonicalBinders) =
                    forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eTout, [Symbol]
bs0')
                  (Expr
eeRenamed, [Symbol]
canonicalBinders') =
                    forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
canonicalBinders (Expr
ee, [Symbol]
bs'')
              forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
dictBinder RFInfo
i
                       RType RTyCon RTyVar RReft
eTin
                       RType RTyCon RTyVar RReft
eToutRenamed
                       (forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
eeRenamed)) Predicate
p)
                , [Symbol]
canonicalBinders'
                )
            | Bool
otherwise = do
              let (RType RTyCon RTyVar RReft
eToutRenamed, [Symbol]
canonicalBinders) =
                    forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eTout, [Symbol]
bs')
                  (Expr
eeRenamed, [Symbol]
canonicalBinders') =
                    forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
canonicalBinders (Expr
ee, [Symbol]
bs'')
              forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
bind RFInfo
i
                       RType RTyCon RTyVar RReft
eTin
                       RType RTyCon RTyVar RReft
eToutRenamed
                       (forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
eeRenamed)) Predicate
p)
                , [Symbol]
canonicalBinders'
                )
      forall a.
PPrint a =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft (Reft
reft, RType RTyCon RTyVar RReft
t) TcRn (RType RTyCon RTyVar RReft, [Symbol])
buildRFunContTrivial [Symbol] -> Expr -> TcRn (RType RTyCon RTyVar RReft, [Symbol])
buildRFunCont

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

    -- support for RankNTypes/ref
    RAllT (RTVar RTyVar
tv RTVInfo (RType RTyCon RTyVar ())
ty) RType RTyCon RTyVar RReft
tout ureft :: RReft
ureft@(MkUReft ref :: Reft
ref@(F.Reft (Symbol
vv, Expr
_oldE)) Predicate
p) -> do
      (RType RTyCon RTyVar RReft
eTout, [Symbol]
bs) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType'
        (PartialSpecType
partialTp forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. f (Free f a) -> Free f a
Free (forall c tv r f. RTVU c tv -> f -> r -> RTypeF c tv r f
RAllTF (forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar RTyVar
tv RTVInfo (RType RTyCon RTyVar ())
ty) (forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) RReft
ureft))
        CoreExpr -> Expr
coreToLogic
        CoreExpr -> TcRn CoreExpr
simplify
        RType RTyCon RTyVar RReft
tout
      forall a.
PPrint a =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft
        (Reft
ref, forall c tv r. tv -> r -> RType c tv r
RVar RTyVar
tv forall a. Monoid a => a
mempty)
        (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar RTyVar
tv RTVInfo (RType RTyCon RTyVar ())
ty) RType RTyCon RTyVar RReft
eTout RReft
ureft, [Symbol]
bs))
        (\[Symbol]
bs' Expr
ee ->
          let (Expr
eeRenamed, [Symbol]
canonicalBinders) =
                forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (Expr
ee, [Symbol]
bs')
          in  forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar RTyVar
tv RTVInfo (RType RTyCon RTyVar ())
ty) RType RTyCon RTyVar RReft
eTout (forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
eeRenamed)) Predicate
p)
                , [Symbol]
canonicalBinders
                )
        )
      -- pure (RAllT (RTVar tv ty) eTout ref, bts')
    -- todo: might as well print an error message?
    RAllP PVU RTyCon RTyVar
pvbind RType RTyCon RTyVar RReft
tout -> do
      (RType RTyCon RTyVar RReft
eTout, [Symbol]
bts') <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType'
        (PartialSpecType
partialTp forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. f (Free f a) -> Free f a
Free (forall c tv r f. PVU c tv -> f -> RTypeF c tv r f
RAllPF PVU RTyCon RTyVar
pvbind (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())))
        CoreExpr -> Expr
coreToLogic
        CoreExpr -> TcRn CoreExpr
simplify
        RType RTyCon RTyVar RReft
tout
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU RTyCon RTyVar
pvbind RType RTyCon RTyVar RReft
eTout, [Symbol]
bts')
    -- pargs not handled for now
    -- RApp tycon args pargs reft
    RApp RTyCon
tycon [RType RTyCon RTyVar RReft]
args [RTProp RTyCon RTyVar RReft]
pargs ureft :: RReft
ureft@(MkUReft reft :: Reft
reft@(F.Reft (Symbol
vv, Expr
_)) Predicate
p)
      | forall c. TyConable c => c -> Bool
isClass RTyCon
tycon -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (RType RTyCon RTyVar RReft
t, [])
      | Bool
otherwise -> do
        [RType RTyCon RTyVar RReft]
args' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM
          (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify)
          [RType RTyCon RTyVar RReft]
args
        forall a.
PPrint a =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft
          (Reft
reft, RType RTyCon RTyVar RReft
t)
          (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
tycon [RType RTyCon RTyVar RReft]
args' [RTProp RTyCon RTyVar RReft]
pargs RReft
ureft, []))
          (\[Symbol]
bs' Expr
ee ->
            forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
tycon [RType RTyCon RTyVar RReft]
args' [RTProp RTyCon RTyVar RReft]
pargs (forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
ee)) Predicate
p), [Symbol]
bs')
          )
    RAppTy RType RTyCon RTyVar RReft
arg RType RTyCon RTyVar RReft
res ureft :: RReft
ureft@(MkUReft reft :: Reft
reft@(F.Reft (Symbol
vv, Expr
_)) Predicate
p) -> do
      (RType RTyCon RTyVar RReft
eArg, [Symbol]
bs ) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
arg
      (RType RTyCon RTyVar RReft
eRes, [Symbol]
bs') <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
res
      let (RType RTyCon RTyVar RReft
eResRenamed, [Symbol]
canonicalBinders) =
            forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eRes, [Symbol]
bs')
      forall a.
PPrint a =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft
        (Reft
reft, RType RTyCon RTyVar RReft
t)
        (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType RTyCon RTyVar RReft
eArg RType RTyCon RTyVar RReft
eResRenamed RReft
ureft, [Symbol]
canonicalBinders))
        (\[Symbol]
bs'' Expr
ee ->
          let (Expr
eeRenamed, [Symbol]
canonicalBinders') =
                forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
canonicalBinders (Expr
ee, [Symbol]
bs'')
          in  forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType RTyCon RTyVar RReft
eArg RType RTyCon RTyVar RReft
eResRenamed (forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
eeRenamed)) Predicate
p)
                , [Symbol]
canonicalBinders'
                )
        )
    -- todo: Existential support
    RAllE Symbol
bind RType RTyCon RTyVar RReft
allarg RType RTyCon RTyVar RReft
ty -> do
      (RType RTyCon RTyVar RReft
eAllarg, [Symbol]
bs ) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
allarg
      (RType RTyCon RTyVar RReft
eTy    , [Symbol]
bs') <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
ty
      let (RType RTyCon RTyVar RReft
eTyRenamed, [Symbol]
canonicalBinders) = forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eTy, [Symbol]
bs')
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
bind RType RTyCon RTyVar RReft
eAllarg RType RTyCon RTyVar RReft
eTyRenamed, [Symbol]
canonicalBinders)
    REx Symbol
bind RType RTyCon RTyVar RReft
allarg RType RTyCon RTyVar RReft
ty -> do
      (RType RTyCon RTyVar RReft
eAllarg, [Symbol]
bs ) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
allarg
      (RType RTyCon RTyVar RReft
eTy    , [Symbol]
bs') <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
ty
      let (RType RTyCon RTyVar RReft
eTyRenamed, [Symbol]
canonicalBinders) = forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eTy, [Symbol]
bs')
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx Symbol
bind RType RTyCon RTyVar RReft
eAllarg RType RTyCon RTyVar RReft
eTyRenamed, [Symbol]
canonicalBinders)
    -- YL: might need to filter RExprArg out and replace RHole with ghc wildcard
    -- in the future
    RExprArg Located Expr
_ -> forall a. Maybe SrcSpan -> [Char] -> a
impossible forall a. Maybe a
Nothing [Char]
"RExprArg should not appear here"
    RHole    RReft
_ -> forall a. Maybe SrcSpan -> [Char] -> a
impossible forall a. Maybe a
Nothing [Char]
"RHole should not appear here"
    RRTy{}     -> forall a. Maybe SrcSpan -> [Char] -> a
todo forall a. Maybe a
Nothing ([Char]
"Not sure how to elaborate RRTy" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp RType RTyCon RTyVar RReft
t)
 where
  boolType :: RType RTyCon RTyVar RReft
boolType = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp (TyCon -> [PVU RTyCon RTyVar] -> TyConInfo -> RTyCon
RTyCon TyCon
boolTyCon [] forall a. Default a => a
def) [] [] forall a. Monoid a => a
mempty :: SpecType
  elaborateReft
    :: (F.PPrint a)
    => (F.Reft, SpecType)
    -> TcRn a
    -> ([F.Symbol] -> F.Expr -> TcRn a)
    -> TcRn a
  elaborateReft :: forall a.
PPrint a =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft (reft :: Reft
reft@(F.Reft (Symbol
vv, Expr
e)), RType RTyCon RTyVar RReft
vvTy) TcRn a
trivial [Symbol] -> Expr -> TcRn a
nonTrivialCont =
    if Reft -> Bool
isTrivial' Reft
reft
      then TcRn a
trivial
      else do
        let
          querySpecType :: RType RTyCon RTyVar RReft
querySpecType =
            RType RTyCon RTyVar RReft
-> PartialSpecType -> RType RTyCon RTyVar RReft
plugType (forall r c tv.
Monoid r =>
RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun' (Bool -> RFInfo
classRFInfo Bool
True) Symbol
vv RType RTyCon RTyVar RReft
vvTy RType RTyCon RTyVar RReft
boolType) PartialSpecType
partialTp :: SpecType

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



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

  grabLams :: ([F.Symbol], F.Expr) -> ([F.Symbol], F.Expr)
  grabLams :: ([Symbol], Expr) -> ([Symbol], Expr)
grabLams ([Symbol]
bs, F.ELam (Symbol
b, Sort
_) Expr
e) = ([Symbol], Expr) -> ([Symbol], Expr)
grabLams (Symbol
b forall a. a -> [a] -> [a]
: [Symbol]
bs, Expr
e)
  grabLams ([Symbol], Expr)
bse                   = ([Symbol], Expr)
bse
  -- dropBinderUnique :: [F.Symbol] -> F.Expr -> F.Expr
  -- dropBinderUnique binders = F.notracepp "ElaboratedExpr"
  --   . F.substa (\x -> if L.elem x binders then GM.dropModuleUnique x else x)

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

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



renameBinderSort :: (F.Symbol -> F.Symbol) -> F.Sort -> F.Sort
renameBinderSort :: (Symbol -> Symbol) -> Sort -> Sort
renameBinderSort Symbol -> Symbol
f = Sort -> Sort
rename
 where
  rename :: Sort -> Sort
rename Sort
F.FInt             = Sort
F.FInt
  rename Sort
F.FReal            = Sort
F.FReal
  rename Sort
F.FNum             = Sort
F.FNum
  rename Sort
F.FFrac            = Sort
F.FFrac
  rename (   F.FObj Symbol
s     ) = Symbol -> Sort
F.FObj (Symbol -> Symbol
f Symbol
s)
  rename t' :: Sort
t'@(F.FVar Int
_     ) = Sort
t'
  rename (   F.FFunc Sort
t0 Sort
t1) = Sort -> Sort -> Sort
F.FFunc (Sort -> Sort
rename Sort
t0) (Sort -> Sort
rename Sort
t1)
  rename (   F.FAbs  Int
x  Sort
t') = Int -> Sort -> Sort
F.FAbs Int
x (Sort -> Sort
rename Sort
t')
  rename t' :: Sort
t'@(F.FTC FTycon
_      ) = Sort
t'
  rename (   F.FApp Sort
t0 Sort
t1 ) = Sort -> Sort -> Sort
F.FApp (Sort -> Sort
rename Sort
t0) (Sort -> Sort
rename Sort
t1)


mkHsTyConApp ::  IdP GhcPs -> [LHsType GhcPs] -> LHsType GhcPs
mkHsTyConApp :: IdP GhcPs -> [LHsType GhcPs] -> LHsType GhcPs
mkHsTyConApp IdP GhcPs
tyconId [LHsType GhcPs]
tyargs = forall (p :: Pass) a.
IsSrcSpanAnn p a =>
LexicalFixity
-> IdP (GhcPass p)
-> [LHsTypeArg (GhcPass p)]
-> LHsType (GhcPass p)
nlHsTyConApp LexicalFixity
Prefix IdP GhcPs
tyconId (forall a b. (a -> b) -> [a] -> [b]
map forall tm ty. tm -> HsArg tm ty
HsValArg [LHsType GhcPs]
tyargs)

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

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

-- FIXME: convert sort to HsType
-- This is currently not doable because how do we know if FInt corresponds to
-- Int or Integer?
fixExprToHsExpr HashSet Symbol
env (F.ECst Expr
e0 Sort
_    ) = HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0
-- fixExprToHsExpr env (F.PAnd []      ) = nlHsVar true_RDR
fixExprToHsExpr HashSet Symbol
_ (F.PAnd []      ) = forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar RdrName
true_RDR
fixExprToHsExpr HashSet Symbol
env (F.PAnd (Expr
e : [Expr]
es)) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
L.foldr Expr -> GenLocated SrcSpanAnnA (HsExpr GhcPs) -> LHsExpr GhcPs
f (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e) [Expr]
es
 where
  f :: Expr -> GenLocated SrcSpanAnnA (HsExpr GhcPs) -> LHsExpr GhcPs
f Expr
x GenLocated SrcSpanAnnA (HsExpr GhcPs)
acc = forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar RdrName
and_RDR) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
x)) GenLocated SrcSpanAnnA (HsExpr GhcPs)
acc

-- This would work in the latest commit
-- fixExprToHsExpr env (F.PAnd es  ) = mkHsApp
--   (nlHsVar (varQual_RDR dATA_FOLDABLE (fsLit "and")))
--   (nlList $ fixExprToHsExpr env <$> es)
fixExprToHsExpr HashSet Symbol
env (F.POr [Expr]
es) = forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
  (forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (Module -> FastString -> RdrName
varQual_RDR Module
dATA_FOLDABLE ([Char] -> FastString
fsLit [Char]
"or")))
  ([LHsExpr GhcPs] -> LHsExpr GhcPs
nlList forall a b. (a -> b) -> a -> b
$ HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
fixExprToHsExpr HashSet Symbol
env (F.PIff Expr
e0 Expr
e1) = forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
  (forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
"<=>"))) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0)
  )
  (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e1)
fixExprToHsExpr HashSet Symbol
env (F.PNot Expr
e) =
  forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar RdrName
not_RDR) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e)
fixExprToHsExpr HashSet Symbol
env (F.PAtom Brel
brel Expr
e0 Expr
e1) = forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
  (forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (Brel -> LHsExpr GhcPs
brelToHsExpr Brel
brel) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0))
  (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e1)
fixExprToHsExpr HashSet Symbol
env (F.PImp Expr
e0 Expr
e1) = forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
  (forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
"==>"))) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0)
  )
  (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e1)

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

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

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

brelToHsExpr :: F.Brel -> LHsExpr GhcPs
brelToHsExpr :: Brel -> LHsExpr GhcPs
brelToHsExpr Brel
brel = forall a an. a -> LocatedAn an a
noLocA (forall p. XVar p -> LIdP p -> HsExpr p
HsVar NoExtField
Ghc.noExtField (forall a an. a -> LocatedAn an a
noLocA (Brel -> RdrName
f Brel
brel)))
 where
  f :: Brel -> RdrName
f Brel
F.Eq = FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
"==")
  f Brel
F.Gt = RdrName
gt_RDR
  f Brel
F.Lt = RdrName
lt_RDR
  f Brel
F.Ge = RdrName
ge_RDR
  f Brel
F.Le = RdrName
le_RDR
  f Brel
F.Ne = FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
"/=")
  f Brel
_    = forall a. Maybe SrcSpan -> [Char] -> a
impossible 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 (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
x HashSet Symbol
env), Just (Char
c, Symbol
_) <- Symbol -> Maybe (Char, Symbol)
F.unconsSym Symbol
s, Char -> Bool
isUpper Char
c = NameSpace
dataName
     | Bool
otherwise = NameSpace
varName


specTypeToLHsType :: SpecType -> LHsType GhcPs
-- surprised that the type application is necessary
specTypeToLHsType :: RType RTyCon RTyVar RReft -> LHsType GhcPs
specTypeToLHsType =
  forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall (w :: * -> *) (f :: * -> *) (m :: * -> *) b a.
(Comonad w, Functor f, Monad m) =>
(forall c. f (w c) -> w (f c))
-> (forall d. m (f d) -> f (m d))
-> (f (w b) -> b)
-> (a -> f (m a))
-> a
-> b
ghylo (forall t a. Corecursive t => Base t (t, a) -> (t, Base t a)
distPara @SpecType) forall (f :: * -> *) a.
Functor f =>
Identity (f a) -> f (Identity a)
distAna) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Recursive t => t -> Base t t
project) forall a b. (a -> b) -> a -> b
$ \case
    RVarF (RTV TyVar
tv) RReft
_ -> forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsType (GhcPass p)
nlHsTyVar
      -- (GM.notracePpr ("varRdr" ++ F.showpp (F.symbol tv)) $ getRdrName tv)
      (NameSpace -> Symbol -> RdrName
symbolToRdrNameNs NameSpace
tvName (forall a. Symbolic a => a -> Symbol
F.symbol TyVar
tv))
    RFunF Symbol
_ RFInfo
_ (RType RTyCon RTyVar RReft
tin, LocatedAn AnnListItem (HsType GhcPs)
tin') (RType RTyCon RTyVar RReft
_, LocatedAn AnnListItem (HsType GhcPs)
tout) RReft
_
      | forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType RTyCon RTyVar RReft
tin -> forall a an. a -> LocatedAn an a
noLocA forall a b. (a -> b) -> a -> b
$ forall pass.
XQualTy pass
-> Maybe (LHsContext pass) -> LHsType pass -> HsType pass
HsQualTy NoExtField
Ghc.noExtField (forall a. a -> Maybe a
Just (forall a an. a -> LocatedAn an a
noLocA [LocatedAn AnnListItem (HsType GhcPs)
tin'])) LocatedAn AnnListItem (HsType GhcPs)
tout
      | Bool
otherwise       -> forall (p :: Pass).
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsFunTy LocatedAn AnnListItem (HsType GhcPs)
tin' LocatedAn AnnListItem (HsType GhcPs)
tout
    RAllTF (forall tv s. RTVar tv s -> tv
ty_var_value -> (RTV TyVar
tv)) (RType RTyCon RTyVar RReft
_, LocatedAn AnnListItem (HsType GhcPs)
t) RReft
_ -> forall a an. a -> LocatedAn an a
noLocA forall a b. (a -> b) -> a -> b
$ forall pass.
XForAllTy pass
-> HsForAllTelescope pass -> LHsType pass -> HsType pass
HsForAllTy
      NoExtField
Ghc.noExtField
      (forall (p :: Pass).
EpAnnForallTy
-> [LHsTyVarBndr Specificity (GhcPass p)]
-> HsForAllTelescope (GhcPass p)
mkHsForAllInvisTele forall a. EpAnn a
noAnn [forall a an. a -> LocatedAn an a
noLocA forall a b. (a -> b) -> a -> b
$ forall flag pass.
XUserTyVar pass -> flag -> LIdP pass -> HsTyVarBndr flag pass
UserTyVar forall a. EpAnn a
noAnn Specificity
SpecifiedSpec (forall a an. a -> LocatedAn an a
noLocA forall a b. (a -> b) -> a -> b
$ NameSpace -> Symbol -> RdrName
symbolToRdrNameNs NameSpace
tvName (forall a. Symbolic a => a -> Symbol
F.symbol TyVar
tv))])
      LocatedAn AnnListItem (HsType GhcPs)
t
    RAllPF PVU RTyCon RTyVar
_ (RType RTyCon RTyVar RReft
_, LocatedAn AnnListItem (HsType GhcPs)
ty)                    -> LocatedAn AnnListItem (HsType GhcPs)
ty
    RAppF RTyCon { rtc_tc :: RTyCon -> TyCon
rtc_tc = TyCon
tc } [(RType RTyCon RTyVar RReft, LocatedAn AnnListItem (HsType GhcPs))]
ts [RTPropF
   RTyCon
   RTyVar
   (RType RTyCon RTyVar RReft, LocatedAn AnnListItem (HsType GhcPs))]
_ RReft
_ -> IdP GhcPs -> [LHsType GhcPs] -> LHsType GhcPs
mkHsTyConApp
      (forall thing. NamedThing thing => thing -> RdrName
getRdrName TyCon
tc)
      [ LocatedAn AnnListItem (HsType GhcPs)
hst | (RType RTyCon RTyVar RReft
t, LocatedAn AnnListItem (HsType GhcPs)
hst) <- [(RType RTyCon RTyVar RReft, LocatedAn AnnListItem (HsType GhcPs))]
ts, forall {c} {tv} {r}. RType c tv r -> Bool
notExprArg RType RTyCon RTyVar RReft
t ]
     where
      notExprArg :: RType c tv r -> Bool
notExprArg (RExprArg Located Expr
_) = Bool
False
      notExprArg RType c tv r
_            = Bool
True
    RAllEF Symbol
_ (RType RTyCon RTyVar RReft
_, LocatedAn AnnListItem (HsType GhcPs)
tin) (RType RTyCon RTyVar RReft
_, LocatedAn AnnListItem (HsType GhcPs)
tout) -> forall (p :: Pass).
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsFunTy LocatedAn AnnListItem (HsType GhcPs)
tin LocatedAn AnnListItem (HsType GhcPs)
tout
    RExF   Symbol
_ (RType RTyCon RTyVar RReft
_, LocatedAn AnnListItem (HsType GhcPs)
tin) (RType RTyCon RTyVar RReft
_, LocatedAn AnnListItem (HsType GhcPs)
tout) -> forall (p :: Pass).
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsFunTy LocatedAn AnnListItem (HsType GhcPs)
tin LocatedAn AnnListItem (HsType GhcPs)
tout
    -- impossible
    RAppTyF (RType RTyCon RTyVar RReft, LocatedAn AnnListItem (HsType GhcPs))
_ (RExprArg Located Expr
_, LocatedAn AnnListItem (HsType GhcPs)
_) RReft
_ ->
      forall a. Maybe SrcSpan -> [Char] -> a
impossible forall a. Maybe a
Nothing [Char]
"RExprArg should not appear here"
    RAppTyF (RType RTyCon RTyVar RReft
_, LocatedAn AnnListItem (HsType GhcPs)
t) (RType RTyCon RTyVar RReft
_, LocatedAn AnnListItem (HsType GhcPs)
t') RReft
_ -> forall (p :: Pass).
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsAppTy LocatedAn AnnListItem (HsType GhcPs)
t LocatedAn AnnListItem (HsType GhcPs)
t'
    -- YL: todo..
    RRTyF [(Symbol,
  (RType RTyCon RTyVar RReft, LocatedAn AnnListItem (HsType GhcPs)))]
_ RReft
_ Oblig
_ (RType RTyCon RTyVar RReft
_, LocatedAn AnnListItem (HsType GhcPs)
t)       -> LocatedAn AnnListItem (HsType GhcPs)
t
    RHoleF RReft
_                 -> forall a an. a -> LocatedAn an a
noLocA forall a b. (a -> b) -> a -> b
$ forall pass. XWildCardTy pass -> HsType pass
HsWildCardTy NoExtField
Ghc.noExtField
    RExprArgF Located Expr
_ ->
      forall a. Maybe SrcSpan -> [Char] -> a
todo forall a. Maybe a
Nothing [Char]
"Oops, specTypeToLHsType doesn't know how to handle RExprArg"