{-# LANGUAGE OverloadedStrings    #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE FlexibleInstances    #-}

{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

-- | This module contains the code that DOES reflection; i.e. converts Haskell
--   definitions into refinements.

module Language.Haskell.Liquid.Bare.Axiom ( makeHaskellAxioms, strengthenSpecWithMeasure, makeAssumeReflectAxioms, AxiomType(..) ) where

import Prelude hiding (error)
import Prelude hiding (mapM)
import qualified Control.Exception         as Ex

-- import           Control.Monad.Except      hiding (forM, mapM)
-- import           Control.Monad.State       hiding (forM, mapM)
import qualified Text.PrettyPrint.HughesPJ as PJ -- (text)
import qualified Data.HashSet              as S
import qualified Data.Maybe                as Mb
import Control.Monad.Trans.State.Lazy (runState, get, put)

import qualified Language.Haskell.Liquid.Measure as Ms
import qualified Language.Fixpoint.Types as F
import qualified Liquid.GHC.API as Ghc
import qualified Language.Haskell.Liquid.GHC.Misc as GM
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Transforms.CoreToLogic
import           Language.Haskell.Liquid.GHC.Misc
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Names
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.Types

import           Language.Haskell.Liquid.Bare.Resolve as Bare
import           Language.Haskell.Liquid.Bare.Types   as Bare
import           Language.Haskell.Liquid.Bare.Measure as Bare
import           Language.Haskell.Liquid.UX.Config
import qualified Data.List as L
import Control.Applicative
import Control.Arrow (second)
import Data.Function (on)
import qualified Data.Map as Map
import qualified Data.HashMap.Strict as M
import System.IO.Unsafe (unsafePerformIO)

findDuplicatePair :: Ord k => (a -> k) -> [a] -> Maybe (a, a)
findDuplicatePair :: forall k a. Ord k => (a -> k) -> [a] -> Maybe (a, a)
findDuplicatePair a -> k
key [a]
xs =
  [(a, a)] -> Maybe (a, a)
forall a. [a] -> Maybe a
Mb.listToMaybe
    [ (a
a, a
b)
    | a
a:a
b:[a]
_ <- (a -> a -> Bool) -> [a] -> [[a]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
L.groupBy (k -> k -> Bool
forall a. Eq a => a -> a -> Bool
(==) (k -> k -> Bool) -> (a -> k) -> a -> a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> k
key) ((a -> k) -> [a] -> [a]
forall b a. Ord b => (a -> b) -> [a] -> [a]
L.sortOn a -> k
key [a]
xs)
    ]

findDuplicateBetweenLists :: (Ord k) => (a -> k) -> [a] -> [a] -> Maybe (a, a)
findDuplicateBetweenLists :: forall k a. Ord k => (a -> k) -> [a] -> [a] -> Maybe (a, a)
findDuplicateBetweenLists a -> k
key [a]
l1 [a]
l2 =
  (a -> k) -> Map k a -> [a] -> Maybe (a, a)
forall k a. Ord k => (a -> k) -> Map k a -> [a] -> Maybe (a, a)
findDuplicate a -> k
key ([(k, a)] -> Map k a
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (a -> k
key a
x, a
x) | a
x <- [a]
l1 ]) [a]
l2
  where
    findDuplicate :: Ord k => (a -> k) -> Map.Map k a -> [a] -> Maybe (a, a)
    findDuplicate :: forall k a. Ord k => (a -> k) -> Map k a -> [a] -> Maybe (a, a)
findDuplicate a -> k
key' Map k a
seen [a]
l2' =
      [(a, a)] -> Maybe (a, a)
forall a. [a] -> Maybe a
Mb.listToMaybe
      [ (a
x, a
y) | a
x <- [a]
l2', Just a
y <- [k -> Map k a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (a -> k
key' a
x) Map k a
seen]]

-----------------------------------------------------------------------------------------------
makeHaskellAxioms :: GhcSrc -> Bare.Env -> Bare.TycEnv -> LogicMap -> GhcSpecSig -> Ms.BareSpec
                  -> Bare.Lookup [(Ghc.Var, LocSpecType, F.Equation)]
-----------------------------------------------------------------------------------------------
makeHaskellAxioms :: GhcSrc
-> Env
-> TycEnv
-> LogicMap
-> GhcSpecSig
-> BareSpec
-> Lookup [(CoreBndr, LocSpecType, Equation)]
makeHaskellAxioms GhcSrc
src Env
env TycEnv
tycEnv LogicMap
lmap GhcSpecSig
spSig BareSpec
spec = do
  let refDefs :: [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)]
refDefs = GhcSrc
-> GhcSpecSig
-> BareSpec
-> Env
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
getReflectDefs GhcSrc
src GhcSpecSig
spSig BareSpec
spec Env
env
  [(CoreBndr, LocSpecType, Equation)]
-> Lookup [(CoreBndr, LocSpecType, Equation)]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
-> TycEnv
-> LogicMap
-> (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
    Expr CoreBndr)
-> (CoreBndr, LocSpecType, Equation)
makeAxiom Env
env TycEnv
tycEnv LogicMap
lmap ((Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)
 -> (CoreBndr, LocSpecType, Equation))
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
-> [(CoreBndr, LocSpecType, Equation)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)]
refDefs)

-----------------------------------------------------------------------------------------------
--          Returns a list of elements, one per assume reflect                               --
-- Each element is made of:                                                                  --
-- * The variable name of the actual function                                                --
-- * The refined type of actual function, where the post-condition is strengthened with      --
--   ``VV == pretendedFn arg1 arg2 ...`                                                      --
-- * The assume reflect equation, linking the pretended and actual function:                 --
--   `actualFn arg1 arg 2 ... = pretendedFn arg1 arg2 ...`                                   --
makeAssumeReflectAxioms :: GhcSrc -> Bare.Env -> Bare.TycEnv -> GhcSpecSig -> Ms.BareSpec
                  -> Bare.Lookup [(Ghc.Var, LocSpecType, F.Equation)]
-----------------------------------------------------------------------------------------------
makeAssumeReflectAxioms :: GhcSrc
-> Env
-> TycEnv
-> GhcSpecSig
-> BareSpec
-> Lookup [(CoreBndr, LocSpecType, Equation)]
makeAssumeReflectAxioms GhcSrc
src Env
env TycEnv
tycEnv GhcSpecSig
spSig BareSpec
spec = do
  -- Send an error message if we're redefining a reflection
  case (Located LHName -> LHName)
-> [Located LHName] -> Maybe (Located LHName, Located LHName)
forall k a. Ord k => (a -> k) -> [a] -> Maybe (a, a)
findDuplicatePair Located LHName -> LHName
forall a. Located a -> a
val [Located LHName]
reflActSymbols Maybe (Located LHName, Located LHName)
-> Maybe (Located LHName, Located LHName)
-> Maybe (Located LHName, Located LHName)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Located LHName -> LHName)
-> [Located LHName]
-> [Located LHName]
-> Maybe (Located LHName, Located LHName)
forall k a. Ord k => (a -> k) -> [a] -> [a] -> Maybe (a, a)
findDuplicateBetweenLists Located LHName -> LHName
forall a. Located a -> a
val [Located LHName]
refSymbols [Located LHName]
reflActSymbols of
    Just (Located LHName
x , Located LHName
y) -> Error -> Lookup [(CoreBndr, LocSpecType, Equation)]
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw (Error -> Lookup [(CoreBndr, LocSpecType, Equation)])
-> Error -> Lookup [(CoreBndr, LocSpecType, Equation)]
forall a b. (a -> b) -> a -> b
$ Located LHName -> [Char] -> Error
forall a. PPrint a => Located a -> [Char] -> Error
mkError Located LHName
y ([Char] -> Error) -> [Char] -> Error
forall a b. (a -> b) -> a -> b
$
                      [Char]
"Duplicate reflection of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                      Located Symbol -> [Char]
forall a. Show a => a -> [Char]
show (HasCallStack => LHName -> Symbol
LHName -> Symbol
lhNameToUnqualifiedSymbol (LHName -> Symbol) -> Located LHName -> Located Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located LHName
x) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                      [Char]
" and " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                      Located Symbol -> [Char]
forall a. Show a => a -> [Char]
show (HasCallStack => LHName -> Symbol
LHName -> Symbol
lhNameToUnqualifiedSymbol (LHName -> Symbol) -> Located LHName -> Located Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located LHName
y)
    Maybe (Located LHName, Located LHName)
Nothing -> [(CoreBndr, LocSpecType, Equation)]
-> Lookup [(CoreBndr, LocSpecType, Equation)]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(CoreBndr, LocSpecType, Equation)]
 -> Lookup [(CoreBndr, LocSpecType, Equation)])
-> [(CoreBndr, LocSpecType, Equation)]
-> Lookup [(CoreBndr, LocSpecType, Equation)]
forall a b. (a -> b) -> a -> b
$ (Located LHName, Located LHName)
-> (CoreBndr, LocSpecType, Equation)
turnIntoAxiom ((Located LHName, Located LHName)
 -> (CoreBndr, LocSpecType, Equation))
-> [(Located LHName, Located LHName)]
-> [(CoreBndr, LocSpecType, Equation)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [(Located LHName, Located LHName)]
forall lname ty.
Spec lname ty -> [(Located LHName, Located LHName)]
Ms.asmReflectSigs BareSpec
spec
  where
    turnIntoAxiom :: (Located LHName, Located LHName)
-> (CoreBndr, LocSpecType, Equation)
turnIntoAxiom (Located LHName
actual, Located LHName
pretended) = GhcSpecSig
-> Env
-> TCEmb TyCon
-> (Located LHName, Located LHName)
-> (CoreBndr, LocSpecType, Equation)
makeAssumeReflectAxiom GhcSpecSig
spSig Env
env TCEmb TyCon
embs (Located LHName
actual, Located LHName
pretended)
    refDefs :: [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)]
refDefs                 = GhcSrc
-> GhcSpecSig
-> BareSpec
-> Env
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
getReflectDefs GhcSrc
src GhcSpecSig
spSig BareSpec
spec Env
env
    embs :: TCEmb TyCon
embs                    = TycEnv -> TCEmb TyCon
Bare.tcEmbs       TycEnv
tycEnv
    refSymbols :: [Located LHName]
refSymbols              =
      (\(Located Symbol
x, Maybe (RType RTyCon RTyVar RReft)
_, CoreBndr
v, Expr CoreBndr
_) -> Located Symbol -> LHName -> Located LHName
forall l b. Loc l => l -> b -> Located b
F.atLoc Located Symbol
x (LHName -> Located LHName) -> LHName -> Located LHName
forall a b. (a -> b) -> a -> b
$ Name -> Symbol -> LHName
makeGHCLHName (CoreBndr -> Name
forall a. NamedThing a => a -> Name
Ghc.getName CoreBndr
v) (CoreBndr -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol CoreBndr
v)) ((Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)
 -> Located LHName)
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
-> [Located LHName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)]
refDefs
    reflActSymbols :: [Located LHName]
reflActSymbols          = (Located LHName, Located LHName) -> Located LHName
forall a b. (a, b) -> a
fst ((Located LHName, Located LHName) -> Located LHName)
-> [(Located LHName, Located LHName)] -> [Located LHName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [(Located LHName, Located LHName)]
forall lname ty.
Spec lname ty -> [(Located LHName, Located LHName)]
Ms.asmReflectSigs BareSpec
spec

-----------------------------------------------------------------------------------------------
-- Processes one `assume reflect` and returns its axiom element, as detailed in              --
-- `makeAssumeReflectAxioms`. Can also be used to compute the updated SpecType of            --
-- a type where we add the post-condition that actual and pretended are the same             --
makeAssumeReflectAxiom :: GhcSpecSig -> Bare.Env -> F.TCEmb Ghc.TyCon
                       -> (Located LHName, Located LHName) -- actual function and pretended function
                       -> (Ghc.Var, LocSpecType, F.Equation)
-----------------------------------------------------------------------------------------------
makeAssumeReflectAxiom :: GhcSpecSig
-> Env
-> TCEmb TyCon
-> (Located LHName, Located LHName)
-> (CoreBndr, LocSpecType, Equation)
makeAssumeReflectAxiom GhcSpecSig
sig Env
env TCEmb TyCon
tce (Located LHName
actual, Located LHName
pretended) =
   -- The actual and pretended function must have the same type
  if Type
pretendedTy Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
actualTy then
    (CoreBndr
actualV, Located LHName
actual{val = aty at}, Equation
actualEq)
  else
    Error -> (CoreBndr, LocSpecType, Equation)
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw (Error -> (CoreBndr, LocSpecType, Equation))
-> Error -> (CoreBndr, LocSpecType, Equation)
forall a b. (a -> b) -> a -> b
$ Located LHName -> [Char] -> Error
forall a. PPrint a => Located a -> [Char] -> Error
mkError Located LHName
actual ([Char] -> Error) -> [Char] -> Error
forall a b. (a -> b) -> a -> b
$
      Symbol -> [Char]
forall a. Show a => a -> [Char]
show Symbol
qPretended [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" and " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show Symbol
qActual [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" should have the same type. But " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"types\n\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
showType Type
pretendedTy [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n and\n\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
showType Type
actualTy  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\ndo not match."
  where
    showType :: Type -> [Char]
showType = DynFlags -> Type -> [Char]
forall a. Outputable a => DynFlags -> a -> [Char]
Ghc.showPpr
      (IO DynFlags -> DynFlags
forall a. IO a -> a
unsafePerformIO (IO DynFlags -> DynFlags) -> IO DynFlags -> DynFlags
forall a b. (a -> b) -> a -> b
$ Ghc DynFlags -> Session -> IO DynFlags
forall a. Ghc a -> Session -> IO a
Ghc.reflectGhc Ghc DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
Ghc.getDynFlags (Session -> IO DynFlags) -> Session -> IO DynFlags
forall a b. (a -> b) -> a -> b
$ GHCTyLookupEnv -> Session
gtleSession (GHCTyLookupEnv -> Session) -> GHCTyLookupEnv -> Session
forall a b. (a -> b) -> a -> b
$ Env -> GHCTyLookupEnv
reTyLookupEnv Env
env)

    at :: AxiomType
at = Located AxiomType -> AxiomType
forall a. Located a -> a
val (Located AxiomType -> AxiomType) -> Located AxiomType -> AxiomType
forall a b. (a -> b) -> a -> b
$ GhcSpecSig
-> Env -> CoreBndr -> Located Symbol -> Located AxiomType
strengthenSpecWithMeasure GhcSpecSig
sig Env
env CoreBndr
actualV Located LHName
pretended{val=qPretended}

    -- Get the Ghc.Var's of the actual and pretended function names
    actualV :: CoreBndr
actualV = case HasCallStack => Env -> Located LHName -> Lookup CoreBndr
Env -> Located LHName -> Lookup CoreBndr
Bare.lookupGhcIdLHName Env
env Located LHName
actual of
      Right CoreBndr
x -> CoreBndr
x
      Left [Error]
_ -> Maybe SrcSpan -> [Char] -> CoreBndr
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located LHName
actual) [Char]
"function to reflect not in scope"
    pretendedV :: CoreBndr
pretendedV = case HasCallStack => Env -> Located LHName -> Lookup CoreBndr
Env -> Located LHName -> Lookup CoreBndr
Bare.lookupGhcIdLHName Env
env Located LHName
pretended of
      Right CoreBndr
x -> CoreBndr
x
      Left [Error]
_ -> Maybe SrcSpan -> [Char] -> CoreBndr
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located LHName
pretended) [Char]
"function to reflect not in scope"
    -- Get the qualified name symbols for the actual and pretended functions
    lhNameToSymbol :: Located LHName -> Symbol
lhNameToSymbol Located LHName
lx =
      Name -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Name -> Symbol) -> Name -> Symbol
forall a b. (a -> b) -> a -> b
$
      Name -> Maybe Name -> Name
forall a. a -> Maybe a -> a
Mb.fromMaybe (Maybe SrcSpan -> [Char] -> Name
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located LHName
lx) ([Char] -> Name) -> [Char] -> Name
forall a b. (a -> b) -> a -> b
$ [Char]
"expected a resolved Haskell name: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Located LHName -> [Char]
forall a. Show a => a -> [Char]
show Located LHName
lx) (Maybe Name -> Name) -> Maybe Name -> Name
forall a b. (a -> b) -> a -> b
$
      LHName -> Maybe Name
getLHGHCName (LHName -> Maybe Name) -> LHName -> Maybe Name
forall a b. (a -> b) -> a -> b
$
      Located LHName -> LHName
forall a. Located a -> a
val Located LHName
lx
    qActual :: Symbol
qActual = Located LHName -> Symbol
lhNameToSymbol Located LHName
actual
    qPretended :: Symbol
qPretended = Located LHName -> Symbol
lhNameToSymbol Located LHName
pretended
    -- Get the GHC type of the actual and pretended functions
    actualTy :: Type
actualTy = CoreBndr -> Type
Ghc.varType CoreBndr
actualV
    pretendedTy :: Type
pretendedTy = CoreBndr -> Type
Ghc.varType CoreBndr
pretendedV

    -- The return type of the function
    out :: Sort
out   = TCEmb TyCon -> RType RTyCon RTyVar RReft -> Sort
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RRType NoReft) r) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce (RType RTyCon RTyVar RReft -> Sort)
-> RType RTyCon RTyVar RReft -> Sort
forall a b. (a -> b) -> a -> b
$ AxiomType -> RType RTyCon RTyVar RReft
ares AxiomType
at
    -- The arguments names and types, as given by `AxiomType`
    xArgs :: [(Symbol, Sort)]
xArgs = (RType RTyCon RTyVar RReft -> Sort)
-> (Symbol, RType RTyCon RTyVar RReft) -> (Symbol, Sort)
forall a b. (a -> b) -> (Symbol, a) -> (Symbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TCEmb TyCon -> RType RTyCon RTyVar RReft -> Sort
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RRType NoReft) r) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce) ((Symbol, RType RTyCon RTyVar RReft) -> (Symbol, Sort))
-> [(Symbol, RType RTyCon RTyVar RReft)] -> [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AxiomType -> [(Symbol, RType RTyCon RTyVar RReft)]
aargs AxiomType
at

    -- Expression of the equation. It is just saying that the actual and pretended functions are the same
    -- when applied to the same arguments
    le :: ExprBV b Symbol
le    = (ExprBV b Symbol -> ExprBV b Symbol -> ExprBV b Symbol)
-> ExprBV b Symbol -> [ExprBV b Symbol] -> ExprBV b Symbol
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ExprBV b Symbol -> ExprBV b Symbol -> ExprBV b Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
F.EApp (Symbol -> ExprBV b Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
qPretended) (Symbol -> ExprBV b Symbol
forall b v. v -> ExprBV b v
F.EVar (Symbol -> ExprBV b Symbol)
-> ((Symbol, Sort) -> Symbol) -> (Symbol, Sort) -> ExprBV b Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Sort) -> ExprBV b Symbol)
-> [(Symbol, Sort)] -> [ExprBV b Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
xArgs)

    actualEq :: Equation
actualEq = Symbol
-> [(Symbol, Sort)] -> ExprBV Symbol Symbol -> Sort -> Equation
F.mkEquation Symbol
qActual [(Symbol, Sort)]
xArgs ExprBV Symbol Symbol
forall {b}. ExprBV b Symbol
le Sort
out

strengthenSpecWithMeasure :: GhcSpecSig -> Bare.Env
                       -> Ghc.Var -- var owning the spec
                       -> LocSymbol     -- measure name
                       -> Located AxiomType
-----------------------------------------------------------------------------------------------
strengthenSpecWithMeasure :: GhcSpecSig
-> Env -> CoreBndr -> Located Symbol -> Located AxiomType
strengthenSpecWithMeasure GhcSpecSig
sig Env
env CoreBndr
actualV Located Symbol
qPretended =
    Located Symbol
qPretended{ val = addSingletonApp allowTC (val qPretended) rt}
  where
    -- Get the GHC type of the actual and pretended functions
    actualTy :: Type
actualTy = CoreBndr -> Type
Ghc.varType CoreBndr
actualV

    -- Compute the refined type of the actual function. See `makeAssumeType` for details
    sigs :: [(CoreBndr, LocSpecType)]
sigs                    = GhcSpecSig -> [(CoreBndr, LocSpecType)]
gsTySigs GhcSpecSig
sig [(CoreBndr, LocSpecType)]
-> [(CoreBndr, LocSpecType)] -> [(CoreBndr, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(CoreBndr, LocSpecType)]
gsAsmSigs GhcSpecSig
sig -- We also look into assumed signatures
    -- Try to get the specification of the actual function from the signatures
    mbT :: Maybe (RType RTyCon RTyVar RReft)
mbT   = LocSpecType -> RType RTyCon RTyVar RReft
forall a. Located a -> a
val (LocSpecType -> RType RTyCon RTyVar RReft)
-> Maybe LocSpecType -> Maybe (RType RTyCon RTyVar RReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreBndr -> [(CoreBndr, LocSpecType)] -> Maybe LocSpecType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup CoreBndr
actualV [(CoreBndr, LocSpecType)]
sigs
    -- Refines that spec. If the specification is not in the scope, just use the GHC type as a dummy spec
    -- to proceed with.
    rt :: RType RTyCon RTyVar RReft
rt    = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
fromRTypeRep (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
 -> RType RTyCon RTyVar RReft)
-> (RType RTyCon RTyVar RReft
    -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            (\trep :: RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep@RTypeRep{[(RTVar RTyVar (RRType NoReft), RReft)]
[Symbol]
[RReft]
[RType RTyCon RTyVar RReft]
[PVarBV Symbol Symbol (RRType NoReft)]
[RFInfo]
RType RTyCon RTyVar RReft
ty_vars :: [(RTVar RTyVar (RRType NoReft), RReft)]
ty_preds :: [PVarBV Symbol Symbol (RRType NoReft)]
ty_binds :: [Symbol]
ty_info :: [RFInfo]
ty_refts :: [RReft]
ty_args :: [RType RTyCon RTyVar RReft]
ty_res :: RType RTyCon RTyVar RReft
ty_res :: forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
ty_args :: forall b v c tv r. RTypeRepBV b v c tv r -> [RTypeBV b v c tv r]
ty_refts :: forall b v c tv r. RTypeRepBV b v c tv r -> [r]
ty_info :: forall b v c tv r. RTypeRepBV b v c tv r -> [RFInfo]
ty_binds :: forall b v c tv r. RTypeRepBV b v c tv r -> [b]
ty_preds :: forall b v c tv r.
RTypeRepBV b v c tv r
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
ty_vars :: forall b v c tv r.
RTypeRepBV b v c tv r
-> [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
..} ->
                RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep{ty_info = fmap (\RFInfo
i -> RFInfo
i{permitTC = Just allowTC}) ty_info}) (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft)
-> (RType RTyCon RTyVar RReft
    -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            RType RTyCon RTyVar RReft
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ RType RTyCon RTyVar RReft
-> Maybe (RType RTyCon RTyVar RReft) -> RType RTyCon RTyVar RReft
forall a. a -> Maybe a -> a
Mb.fromMaybe (Type -> RType RTyCon RTyVar RReft
forall r. IsReft r => Type -> RRType r
ofType Type
actualTy) Maybe (RType RTyCon RTyVar RReft)
mbT
    allowTC :: Bool
allowTC = Config -> Bool
typeclass (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)

-- Gets the definitions of all the symbols that `BareSpec` wants to reflect.
--
-- Because we allow to name private variables here, not all symbols can easily
-- be turned into `Ghc.Var`. Essentially, `findVarDefType` can initially only
-- fetch the definitions of public variables. We use a fixpoint so that for each
-- newly retrieved definition, we get the list of variables used inside it and
-- record them in a HashMap so that in the next round, we might be able to get
-- more definitions (because once you have a variable, it's easy to get its
-- unfolding).
--
-- Iterates until no new definition is found. In which case, we fail
-- if there are still symbols left which we failed to find the source for.
getReflectDefs :: GhcSrc -> GhcSpecSig -> Ms.BareSpec -> Bare.Env
               -> [(LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr)]
getReflectDefs :: GhcSrc
-> GhcSpecSig
-> BareSpec
-> Env
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
getReflectDefs GhcSrc
src GhcSpecSig
sig BareSpec
spec Env
env =
  [Either (Located LHName) (Located Symbol)]
-> HashMap (Located Symbol) CoreBndr
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
searchInTransitiveClosure [Either (Located LHName) (Located Symbol)]
symsToResolve HashMap (Located Symbol) CoreBndr
forall {k} {v}. HashMap k v
initialDefinedMap []
  where
    sigs :: [(CoreBndr, LocSpecType)]
sigs                    = GhcSpecSig -> [(CoreBndr, LocSpecType)]
gsTySigs GhcSpecSig
sig
    symsToResolve :: [Either (Located LHName) (Located Symbol)]
symsToResolve =
      (Located LHName -> Either (Located LHName) (Located Symbol))
-> [Located LHName] -> [Either (Located LHName) (Located Symbol)]
forall a b. (a -> b) -> [a] -> [b]
map Located LHName -> Either (Located LHName) (Located Symbol)
forall a b. a -> Either a b
Left (HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
S.toList (BareSpec -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.reflects BareSpec
spec)) [Either (Located LHName) (Located Symbol)]
-> [Either (Located LHName) (Located Symbol)]
-> [Either (Located LHName) (Located Symbol)]
forall a. [a] -> [a] -> [a]
++
      (Located Symbol -> Either (Located LHName) (Located Symbol))
-> [Located Symbol] -> [Either (Located LHName) (Located Symbol)]
forall a b. (a -> b) -> [a] -> [b]
map Located Symbol -> Either (Located LHName) (Located Symbol)
forall a b. b -> Either a b
Right (HashSet (Located Symbol) -> [Located Symbol]
forall a. HashSet a -> [a]
S.toList (BareSpec -> HashSet (Located Symbol)
forall lname ty. Spec lname ty -> HashSet (Located Symbol)
Ms.privateReflects BareSpec
spec))
    cbs :: [(CoreBndr, Expr CoreBndr)]
cbs = [Bind CoreBndr] -> [(CoreBndr, Expr CoreBndr)]
forall b. [Bind b] -> [(b, Expr b)]
Ghc.flattenBinds ([Bind CoreBndr] -> [(CoreBndr, Expr CoreBndr)])
-> [Bind CoreBndr] -> [(CoreBndr, Expr CoreBndr)]
forall a b. (a -> b) -> a -> b
$ GhcSrc -> [Bind CoreBndr]
_giCbs GhcSrc
src
    initialDefinedMap :: HashMap k v
initialDefinedMap          = HashMap k v
forall {k} {v}. HashMap k v
M.empty

    -- First argument of the `searchInTransitiveClosure` function should always
    -- decrease.
    -- The second argument contains the Vars that appear free in the definitions
    -- of the symbols in the third argument.
    -- The third argument contains the symbols that have been resolved.
    --
    -- The set of symbols in the union of the first and third argument should
    -- remain constant in every recursive call. Moreover, both arguments are
    -- disjoint.
    --
    -- Base case: No symbols left to resolve - we're good
    searchInTransitiveClosure :: [Either (Located LHName) (Located Symbol)]
-> HashMap (Located Symbol) CoreBndr
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
searchInTransitiveClosure [] HashMap (Located Symbol) CoreBndr
_ [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)]
acc = [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)]
acc
    -- Recursive case: there are some left.
    searchInTransitiveClosure [Either (Located LHName) (Located Symbol)]
toResolve HashMap (Located Symbol) CoreBndr
fvMap [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)]
acc = if [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)]
-> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)]
found
         then case [Either (Located LHName) (Located Symbol)]
newToResolve of
                -- No one newly found but no one left to process - we're good
                [] -> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)]
acc
                -- No one newly found but at least one symbol left - we throw
                -- an error
                Either (Located LHName) (Located Symbol)
x:[Either (Located LHName) (Located Symbol)]
_ -> Error
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw (Error
 -> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
      Expr CoreBndr)])
-> ([Char] -> Error)
-> [Char]
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located LHName -> [Char] -> Error)
-> (Located Symbol -> [Char] -> Error)
-> Either (Located LHName) (Located Symbol)
-> [Char]
-> Error
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Located LHName -> [Char] -> Error
forall a. PPrint a => Located a -> [Char] -> Error
mkError Located Symbol -> [Char] -> Error
forall a. PPrint a => Located a -> [Char] -> Error
mkError Either (Located LHName) (Located Symbol)
x ([Char]
 -> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
      Expr CoreBndr)])
-> [Char]
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
forall a b. (a -> b) -> a -> b
$
                  [Char]
"Not found in scope nor in the amongst these variables: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                    (CoreBndr -> [Char] -> [Char])
-> [Char] -> HashMap (Located Symbol) CoreBndr -> [Char]
forall a b. (a -> b -> b) -> b -> HashMap (Located Symbol) a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\CoreBndr
x1 [Char]
acc1 -> [Char]
acc1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" , " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CoreBndr -> [Char]
forall a. Show a => a -> [Char]
show CoreBndr
x1) [Char]
"" HashMap (Located Symbol) CoreBndr
newFvMap
         else [Either (Located LHName) (Located Symbol)]
-> HashMap (Located Symbol) CoreBndr
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
searchInTransitiveClosure [Either (Located LHName) (Located Symbol)]
newToResolve HashMap (Located Symbol) CoreBndr
newFvMap [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)]
newAcc
      where
        -- Try to get the definitions of the symbols that are left (`toResolve`)
        resolvedSyms :: [Maybe
   (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
    Expr CoreBndr)]
resolvedSyms = [(CoreBndr, Expr CoreBndr)]
-> [(CoreBndr, LocSpecType)]
-> Env
-> HashMap (Located Symbol) CoreBndr
-> Either (Located LHName) (Located Symbol)
-> Maybe
     (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
      Expr CoreBndr)
findVarDefType [(CoreBndr, Expr CoreBndr)]
cbs [(CoreBndr, LocSpecType)]
sigs Env
env HashMap (Located Symbol) CoreBndr
fvMap (Either (Located LHName) (Located Symbol)
 -> Maybe
      (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
       Expr CoreBndr))
-> [Either (Located LHName) (Located Symbol)]
-> [Maybe
      (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
       Expr CoreBndr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Either (Located LHName) (Located Symbol)]
toResolve
        -- Collect the newly found definitions
        found :: [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)]
found     = [Maybe
   (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
    Expr CoreBndr)]
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
forall a. [Maybe a] -> [a]
Mb.catMaybes [Maybe
   (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
    Expr CoreBndr)]
resolvedSyms
        -- Add them to the accumulator
        newAcc :: [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)]
newAcc    = [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)]
acc [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)]
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
forall a. [a] -> [a] -> [a]
++ [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)]
found
        -- Add any variable occurrence in them to `fvMap`
        newFvMap :: HashMap (Located Symbol) CoreBndr
newFvMap = (HashMap (Located Symbol) CoreBndr
 -> (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)
 -> HashMap (Located Symbol) CoreBndr)
-> HashMap (Located Symbol) CoreBndr
-> [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
     Expr CoreBndr)]
-> HashMap (Located Symbol) CoreBndr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl HashMap (Located Symbol) CoreBndr
-> (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
    Expr CoreBndr)
-> HashMap (Located Symbol) CoreBndr
forall {a} {b} {c}.
HashMap (Located Symbol) CoreBndr
-> (a, b, c, Expr CoreBndr) -> HashMap (Located Symbol) CoreBndr
addFreeVarsToMap HashMap (Located Symbol) CoreBndr
fvMap [(Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
  Expr CoreBndr)]
found
        -- Collect all the symbols that still failed to be resolved in this
        -- iteration
        newToResolve :: [Either (Located LHName) (Located Symbol)]
newToResolve = [Either (Located LHName) (Located Symbol)
x | (Either (Located LHName) (Located Symbol)
x, Maybe
  (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
   Expr CoreBndr)
Nothing) <- [Either (Located LHName) (Located Symbol)]
-> [Maybe
      (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
       Expr CoreBndr)]
-> [(Either (Located LHName) (Located Symbol),
     Maybe
       (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
        Expr CoreBndr))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Either (Located LHName) (Located Symbol)]
toResolve [Maybe
   (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
    Expr CoreBndr)]
resolvedSyms]

    -- Collects the free variables in an expression and inserts them to the
    -- provided map between symbols and variables. Especially useful to collect
    -- private variables, since it's the only way to reach them (seeing them in
    -- other unfoldings)
    addFreeVarsToMap :: HashMap (Located Symbol) CoreBndr
-> (a, b, c, Expr CoreBndr) -> HashMap (Located Symbol) CoreBndr
addFreeVarsToMap HashMap (Located Symbol) CoreBndr
fvMap (a
_, b
_, c
_, Expr CoreBndr
expr) =
      let freeVarsSet :: [CoreBndr]
freeVarsSet = Expr CoreBndr -> [CoreBndr]
getAllFreeVars Expr CoreBndr
expr
          newVars :: HashMap (Located Symbol) CoreBndr
newVars =
            [(Located Symbol, CoreBndr)] -> HashMap (Located Symbol) CoreBndr
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [(CoreBndr -> Located Symbol
Bare.varLocSym CoreBndr
var, CoreBndr
var) | CoreBndr
var <- [CoreBndr]
freeVarsSet]
      in HashMap (Located Symbol) CoreBndr
-> HashMap (Located Symbol) CoreBndr
-> HashMap (Located Symbol) CoreBndr
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
M.union HashMap (Located Symbol) CoreBndr
fvMap HashMap (Located Symbol) CoreBndr
newVars

    getAllFreeVars :: Expr CoreBndr -> [CoreBndr]
getAllFreeVars = InterestingVarFun -> Expr CoreBndr -> [CoreBndr]
Ghc.exprSomeFreeVarsList (Bool -> InterestingVarFun
forall a b. a -> b -> a
const Bool
True)

-- | Names for functions that need to be reflected
--
-- > Left nameInScope | Right qualifiedPrivateName
type ToReflectName = Either (Located LHName) LocSymbol

-- Finds the definition of a variable in the given Core binds, or in the
-- unfoldings of a Var. Used for reflection. Returns the same
-- `LHName` given as argument, the SpecType of this symbol, its corresponding
-- variable and definition (the `CoreExpr`).
--
-- Takes as arguments:
-- - The list of bindings, usually taken from the GhcSrc
-- - A map of signatures, used to retrieve the `SpecType`
-- - The current environment, that can be used to resolve symbols
-- - An extra map between symbols and variables for those symbols that are hard
--   to resolve, especially if they are private symbols from foreign
--   dependencies. This map will be used as a fallback if the default resolving
--   mechanism fails.
--
-- Returns `Nothing` iff the symbol could not be resolved. No error is thrown in
-- this case since this function is used by the fixpoint mechanism of
-- `getReflectDefs`. Which will collect all the symbols that could (not) yet be
-- resolved.
--
-- Errors can be raised whenever the symbol was found but the rest of the
-- process failed (no unfoldings available, lifted functions not exported,
-- etc.).
findVarDefType :: [(Ghc.Id, Ghc.CoreExpr)] -> [(Ghc.Var, LocSpecType)] -> Bare.Env
               -> M.HashMap LocSymbol Ghc.Var -> ToReflectName
               -> Maybe (LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr)
findVarDefType :: [(CoreBndr, Expr CoreBndr)]
-> [(CoreBndr, LocSpecType)]
-> Env
-> HashMap (Located Symbol) CoreBndr
-> Either (Located LHName) (Located Symbol)
-> Maybe
     (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
      Expr CoreBndr)
findVarDefType [(CoreBndr, Expr CoreBndr)]
cbs [(CoreBndr, LocSpecType)]
sigs Env
env HashMap (Located Symbol) CoreBndr
_defs (Left Located LHName
x) =
  case ((CoreBndr, Expr CoreBndr) -> Bool)
-> [(CoreBndr, Expr CoreBndr)] -> Maybe (CoreBndr, Expr CoreBndr)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find ((Located LHName -> LHName
forall a. Located a -> a
val Located LHName
x LHName -> LHName -> Bool
forall a. Eq a => a -> a -> Bool
==) (LHName -> Bool)
-> ((CoreBndr, Expr CoreBndr) -> LHName)
-> (CoreBndr, Expr CoreBndr)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreBndr -> LHName
makeGHCLHNameFromId (CoreBndr -> LHName)
-> ((CoreBndr, Expr CoreBndr) -> CoreBndr)
-> (CoreBndr, Expr CoreBndr)
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CoreBndr, Expr CoreBndr) -> CoreBndr
forall a b. (a, b) -> a
fst) [(CoreBndr, Expr CoreBndr)]
cbs of
  -- YL: probably ok even without checking typeclass flag since user cannot
  -- manually reflect internal names
  Just (CoreBndr
v, Expr CoreBndr
e) ->
    (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
 Expr CoreBndr)
-> Maybe
     (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
      Expr CoreBndr)
forall a. a -> Maybe a
Just ((LHName -> Symbol) -> Located LHName -> Located Symbol
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHName -> Symbol
getLHNameSymbol Located LHName
x, LocSpecType -> RType RTyCon RTyVar RReft
forall a. Located a -> a
val (LocSpecType -> RType RTyCon RTyVar RReft)
-> Maybe LocSpecType -> Maybe (RType RTyCon RTyVar RReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreBndr -> [(CoreBndr, LocSpecType)] -> Maybe LocSpecType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup CoreBndr
v [(CoreBndr, LocSpecType)]
sigs, CoreBndr
v, Expr CoreBndr
e)
  Maybe (CoreBndr, Expr CoreBndr)
Nothing     -> do
    let ecall :: a
ecall = Maybe SrcSpan -> [Char] -> a
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located LHName
x) [Char]
"function to reflect not found"
        var :: CoreBndr
var = ([Error] -> CoreBndr)
-> (CoreBndr -> CoreBndr) -> Lookup CoreBndr -> CoreBndr
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either [Error] -> CoreBndr
forall {a}. a
ecall CoreBndr -> CoreBndr
forall a. a -> a
id (HasCallStack => Env -> Located LHName -> Lookup CoreBndr
Env -> Located LHName -> Lookup CoreBndr
Bare.lookupGhcIdLHName Env
env Located LHName
x)
        info :: IdInfo
info = HasDebugCallStack => CoreBndr -> IdInfo
CoreBndr -> IdInfo
Ghc.idInfo CoreBndr
var
        unfolding :: Maybe (Expr CoreBndr)
unfolding = Unfolding -> Maybe (Expr CoreBndr)
getExprFromUnfolding (Unfolding -> Maybe (Expr CoreBndr))
-> (IdInfo -> Unfolding) -> IdInfo -> Maybe (Expr CoreBndr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IdInfo -> Unfolding
Ghc.realUnfoldingInfo (IdInfo -> Maybe (Expr CoreBndr))
-> IdInfo -> Maybe (Expr CoreBndr)
forall a b. (a -> b) -> a -> b
$ IdInfo
info
    case Maybe (Expr CoreBndr)
unfolding of
      Just Expr CoreBndr
e ->
        (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
 Expr CoreBndr)
-> Maybe
     (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
      Expr CoreBndr)
forall a. a -> Maybe a
Just ((LHName -> Symbol) -> Located LHName -> Located Symbol
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHName -> Symbol
getLHNameSymbol Located LHName
x, LocSpecType -> RType RTyCon RTyVar RReft
forall a. Located a -> a
val (LocSpecType -> RType RTyCon RTyVar RReft)
-> Maybe LocSpecType -> Maybe (RType RTyCon RTyVar RReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreBndr -> [(CoreBndr, LocSpecType)] -> Maybe LocSpecType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup CoreBndr
var [(CoreBndr, LocSpecType)]
sigs, CoreBndr
var, Expr CoreBndr
e)
      Maybe (Expr CoreBndr)
_ ->
        Error
-> Maybe
     (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
      Expr CoreBndr)
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw (Error
 -> Maybe
      (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
       Expr CoreBndr))
-> Error
-> Maybe
     (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
      Expr CoreBndr)
forall a b. (a -> b) -> a -> b
$ Located LHName -> [Char] -> Error
forall a. PPrint a => Located a -> [Char] -> Error
mkError Located LHName
x ([Char] -> Error) -> [Char] -> Error
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords
          [ [Char]
"Symbol exists but is not defined in the current file,"
          , [Char]
"and no unfolding is available in the interface files"
          ]

findVarDefType [(CoreBndr, Expr CoreBndr)]
_cbs [(CoreBndr, LocSpecType)]
sigs Env
_env HashMap (Located Symbol) CoreBndr
defs (Right Located Symbol
x) = do
    var <- Located Symbol
-> HashMap (Located Symbol) CoreBndr -> Maybe CoreBndr
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Located Symbol
x HashMap (Located Symbol) CoreBndr
defs
    let info = HasDebugCallStack => CoreBndr -> IdInfo
CoreBndr -> IdInfo
Ghc.idInfo CoreBndr
var
    let unfolding = Unfolding -> Maybe (Expr CoreBndr)
getExprFromUnfolding (Unfolding -> Maybe (Expr CoreBndr))
-> (IdInfo -> Unfolding) -> IdInfo -> Maybe (Expr CoreBndr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IdInfo -> Unfolding
Ghc.realUnfoldingInfo (IdInfo -> Maybe (Expr CoreBndr))
-> IdInfo -> Maybe (Expr CoreBndr)
forall a b. (a -> b) -> a -> b
$ IdInfo
info
    case unfolding of
      Just Expr CoreBndr
e ->
        (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
 Expr CoreBndr)
-> Maybe
     (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
      Expr CoreBndr)
forall a. a -> Maybe a
Just (Located Symbol
x, LocSpecType -> RType RTyCon RTyVar RReft
forall a. Located a -> a
val (LocSpecType -> RType RTyCon RTyVar RReft)
-> Maybe LocSpecType -> Maybe (RType RTyCon RTyVar RReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreBndr -> [(CoreBndr, LocSpecType)] -> Maybe LocSpecType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup CoreBndr
var [(CoreBndr, LocSpecType)]
sigs, CoreBndr
var, Expr CoreBndr
e)
      Maybe (Expr CoreBndr)
_ ->
        Error
-> Maybe
     (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
      Expr CoreBndr)
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw (Error
 -> Maybe
      (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
       Expr CoreBndr))
-> Error
-> Maybe
     (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
      Expr CoreBndr)
forall a b. (a -> b) -> a -> b
$ Located Symbol -> [Char] -> Error
forall a. PPrint a => Located a -> [Char] -> Error
mkError Located Symbol
x ([Char] -> Error) -> [Char] -> Error
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords
          [ [Char]
"Symbol exists but is not defined in the current file,"
          , [Char]
"and no unfolding is available in the interface files"
          ]

getExprFromUnfolding :: Ghc.Unfolding -> Maybe Ghc.CoreExpr
getExprFromUnfolding :: Unfolding -> Maybe (Expr CoreBndr)
getExprFromUnfolding (Ghc.CoreUnfolding Expr CoreBndr
expr UnfoldingSource
_ Bool
_ UnfoldingCache
_ UnfoldingGuidance
_) = Expr CoreBndr -> Maybe (Expr CoreBndr)
forall a. a -> Maybe a
Just Expr CoreBndr
expr
getExprFromUnfolding Unfolding
_ = Maybe (Expr CoreBndr)
forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
makeAxiom :: Bare.Env -> Bare.TycEnv -> LogicMap
          -> (LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr)
          -> (Ghc.Var, LocSpecType, F.Equation)
--------------------------------------------------------------------------------
makeAxiom :: Env
-> TycEnv
-> LogicMap
-> (Located Symbol, Maybe (RType RTyCon RTyVar RReft), CoreBndr,
    Expr CoreBndr)
-> (CoreBndr, LocSpecType, Equation)
makeAxiom Env
env TycEnv
tycEnv LogicMap
lmap (Located Symbol
x, Maybe (RType RTyCon RTyVar RReft)
mbT, CoreBndr
v, Expr CoreBndr
def)
            = (CoreBndr
v, LocSpecType
t, Equation
e)
  where
    (LocSpecType
t, Equation
e)  = Config
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> Located Symbol
-> Maybe (RType RTyCon RTyVar RReft)
-> CoreBndr
-> Expr CoreBndr
-> (LocSpecType, Equation)
makeAssumeType (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env) TCEmb TyCon
embs LogicMap
lmap DataConMap
dm Located Symbol
x Maybe (RType RTyCon RTyVar RReft)
mbT CoreBndr
v Expr CoreBndr
def
    embs :: TCEmb TyCon
embs    = TycEnv -> TCEmb TyCon
Bare.tcEmbs       TycEnv
tycEnv
    dm :: DataConMap
dm      = TycEnv -> DataConMap
Bare.tcDataConMap TycEnv
tycEnv

mkError :: PPrint a => Located a -> String -> Error
mkError :: forall a. PPrint a => Located a -> [Char] -> Error
mkError Located a
x [Char]
str = SrcSpan -> Doc -> Doc -> Error
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrHMeas (SourcePos -> SrcSpan
sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Located a -> SourcePos
forall a. Located a -> SourcePos
loc Located a
x) (a -> Doc
forall a. PPrint a => a -> Doc
pprint (a -> Doc) -> a -> Doc
forall a b. (a -> b) -> a -> b
$ Located a -> a
forall a. Located a -> a
val Located a
x) ([Char] -> Doc
PJ.text [Char]
str)

-- This function is uded to generate the fixpoint code for reflected functions
makeAssumeType
  :: Config
  -> F.TCEmb Ghc.TyCon -> LogicMap -> DataConMap -> LocSymbol -> Maybe SpecType
  -> Ghc.Var -> Ghc.CoreExpr
  -> (LocSpecType, F.Equation)
makeAssumeType :: Config
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> Located Symbol
-> Maybe (RType RTyCon RTyVar RReft)
-> CoreBndr
-> Expr CoreBndr
-> (LocSpecType, Equation)
makeAssumeType Config
cfg TCEmb TyCon
tce LogicMap
lmap DataConMap
dm Located Symbol
sym Maybe (RType RTyCon RTyVar RReft)
mbT CoreBndr
v Expr CoreBndr
def
  = ( Located Symbol
sym {val = aty at `strengthenRes` F.subst su ref}
    , Symbol
-> [(Symbol, Sort)] -> ExprBV Symbol Symbol -> Sort -> Equation
F.mkEquation
        Symbol
symbolV
        (((Symbol, Sort) -> (Symbol, Sort))
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Sort -> Sort) -> (Symbol, Sort) -> (Symbol, Sort)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((Sort -> Sort) -> (Symbol, Sort) -> (Symbol, Sort))
-> (Sort -> Sort) -> (Symbol, Sort) -> (Symbol, Sort)
forall a b. (a -> b) -> a -> b
$ SortSubst -> Sort -> Sort
F.sortSubst SortSubst
sortSub) [(Symbol, Sort)]
xts)
        (SortSubst -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
F.sortSubstInExpr SortSubst
sortSub (SubstV (Variable (ExprBV Symbol Symbol))
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV Symbol
SubstV (Variable (ExprBV Symbol Symbol))
su ExprBV Symbol Symbol
le))
        (SortSubst -> Sort -> Sort
F.sortSubst SortSubst
sortSub Sort
out)
    )
  where
    allowTC :: Bool
allowTC = Config -> Bool
typeclass Config
cfg
    symbolV :: Symbol
symbolV = CoreBndr -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol CoreBndr
v
    rt :: RType RTyCon RTyVar RReft
rt    = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
fromRTypeRep (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
 -> RType RTyCon RTyVar RReft)
-> (RType RTyCon RTyVar RReft
    -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            (\trep :: RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep@RTypeRep{[(RTVar RTyVar (RRType NoReft), RReft)]
[Symbol]
[RReft]
[RType RTyCon RTyVar RReft]
[PVarBV Symbol Symbol (RRType NoReft)]
[RFInfo]
RType RTyCon RTyVar RReft
ty_res :: forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
ty_args :: forall b v c tv r. RTypeRepBV b v c tv r -> [RTypeBV b v c tv r]
ty_refts :: forall b v c tv r. RTypeRepBV b v c tv r -> [r]
ty_info :: forall b v c tv r. RTypeRepBV b v c tv r -> [RFInfo]
ty_binds :: forall b v c tv r. RTypeRepBV b v c tv r -> [b]
ty_preds :: forall b v c tv r.
RTypeRepBV b v c tv r
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
ty_vars :: forall b v c tv r.
RTypeRepBV b v c tv r
-> [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
ty_vars :: [(RTVar RTyVar (RRType NoReft), RReft)]
ty_preds :: [PVarBV Symbol Symbol (RRType NoReft)]
ty_binds :: [Symbol]
ty_info :: [RFInfo]
ty_refts :: [RReft]
ty_args :: [RType RTyCon RTyVar RReft]
ty_res :: RType RTyCon RTyVar RReft
..} ->
                RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep{ty_info = fmap (\RFInfo
i -> RFInfo
i{permitTC = Just allowTC}) ty_info}) (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft)
-> (RType RTyCon RTyVar RReft
    -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            RType RTyCon RTyVar RReft
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ RType RTyCon RTyVar RReft
-> Maybe (RType RTyCon RTyVar RReft) -> RType RTyCon RTyVar RReft
forall a. a -> Maybe a -> a
Mb.fromMaybe (Type -> RType RTyCon RTyVar RReft
forall r. IsReft r => Type -> RRType r
ofType Type
τ) Maybe (RType RTyCon RTyVar RReft)
mbT
    τ :: Type
τ     = CoreBndr -> Type
Ghc.varType CoreBndr
v
    at :: AxiomType
at    = Bool -> Symbol -> RType RTyCon RTyVar RReft -> AxiomType
addSingletonApp Bool
allowTC Symbol
symbolV RType RTyCon RTyVar RReft
rt
    out :: Sort
out   = TCEmb TyCon -> RType RTyCon RTyVar RReft -> Sort
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RRType NoReft) r) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce (RType RTyCon RTyVar RReft -> Sort)
-> RType RTyCon RTyVar RReft -> Sort
forall a b. (a -> b) -> a -> b
$ AxiomType -> RType RTyCon RTyVar RReft
ares AxiomType
at
    xArgs :: [ExprBV b Symbol]
xArgs = Symbol -> ExprBV b Symbol
forall b v. v -> ExprBV b v
F.EVar (Symbol -> ExprBV b Symbol)
-> ((Symbol, RType RTyCon RTyVar RReft) -> Symbol)
-> (Symbol, RType RTyCon RTyVar RReft)
-> ExprBV b Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, RType RTyCon RTyVar RReft) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, RType RTyCon RTyVar RReft) -> ExprBV b Symbol)
-> [(Symbol, RType RTyCon RTyVar RReft)] -> [ExprBV b Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AxiomType -> [(Symbol, RType RTyCon RTyVar RReft)]
aargs AxiomType
at
    _msg :: [Char]
_msg  = [[Char]] -> [Char]
unwords [Located Symbol -> [Char]
forall a. PPrint a => a -> [Char]
showpp Located Symbol
sym, Maybe (RType RTyCon RTyVar RReft) -> [Char]
forall a. PPrint a => a -> [Char]
showpp Maybe (RType RTyCon RTyVar RReft)
mbT]
    le :: ExprBV Symbol Symbol
le    = case [CoreBndr]
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> Config
-> ([Char] -> Error)
-> LogicM (ExprBV Symbol Symbol)
-> Either Error (ExprBV Symbol Symbol)
forall t.
[CoreBndr]
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> Config
-> ([Char] -> Error)
-> LogicM t
-> Either Error t
runToLogicWithBoolBinds [CoreBndr]
bbs TCEmb TyCon
tce LogicMap
lmap DataConMap
dm Config
cfg [Char] -> Error
forall {t}. [Char] -> TError t
mkErr (Expr CoreBndr -> LogicM (ExprBV Symbol Symbol)
coreToLogic Expr CoreBndr
def') of
              Right ExprBV Symbol Symbol
e -> ExprBV Symbol Symbol
e
              Left  Error
e -> Error -> ExprBV Symbol Symbol
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw Error
e
    ref :: ReftBV Symbol Symbol
ref        = (Symbol, ExprBV Symbol Symbol) -> ReftBV Symbol Symbol
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (Symbol
F.vv_, 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
F.Eq (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
F.vv_) ExprBV Symbol Symbol
le)
    mkErr :: [Char] -> TError t
mkErr [Char]
s    = SrcSpan -> Doc -> Doc -> TError t
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrHMeas (SourcePos -> SrcSpan
sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Located Symbol -> SourcePos
forall a. Located a -> SourcePos
loc Located Symbol
sym) (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (Symbol -> Doc) -> Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ Located Symbol -> Symbol
forall a. Located a -> a
val Located Symbol
sym) ([Char] -> Doc
PJ.text [Char]
s)
    bbs :: [CoreBndr]
bbs        = InterestingVarFun -> [CoreBndr] -> [CoreBndr]
forall a. (a -> Bool) -> [a] -> [a]
filter InterestingVarFun
isBoolBind [CoreBndr]
xs

    -- rTypeSortExp produces monomorphic sorts from polymorphic types.
    -- As an example, for
    -- id :: a -> a ... id x = x
    -- we got:
    -- define id (x : a#foobar) : a#foobar = { (x : a#foobar) }
    -- Using FObj instead of a real type variable (FVar i) This code solves the
    -- issue by creating a sort substitution that replaces those "fake" type variables
    -- with actual ones.
    -- define id (x : @-1) : a@-1 = { (x : a@-1) }
    ([CoreBndr]
tyVars, Type
_) = Type -> ([CoreBndr], Type)
Ghc.splitForAllTyCoVars Type
τ
    sortSub :: SortSubst
sortSub     = [(Symbol, Sort)] -> SortSubst
F.mkSortSubst ([(Symbol, Sort)] -> SortSubst) -> [(Symbol, Sort)] -> SortSubst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Sort] -> [(Symbol, Sort)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((CoreBndr -> Symbol) -> [CoreBndr] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CoreBndr -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol [CoreBndr]
tyVars) (Int -> Sort
F.FVar (Int -> Sort) -> [Int] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int]
freeSort)
    -- We need sorts that aren't polluted by rank-n types, we can't just look at
    -- the term to determine statically what is the "maximum" sort bound ex:
    -- freeSort = [1 + (maximum $ -1 : F.sortAbs out : fmap (F.sortAbs . snd) xts) ..]
    -- as some variable may be bound to something of rank-n type.  In
    -- SortCheck.hs in fixpoint they just start at 42 for some reason.  I think
    -- Negative Debruijn indices (levels :^)) are safer
    freeSort :: [Int]
freeSort    = [-Int
1, -Int
2 ..]

    ([CoreBndr]
xs, Expr CoreBndr
def') =
      [Char]
-> ([CoreBndr], Expr CoreBndr) -> ([CoreBndr], Expr CoreBndr)
forall a. Outputable a => [Char] -> a -> a
GM.notracePpr [Char]
"grabBody" (([CoreBndr], Expr CoreBndr) -> ([CoreBndr], Expr CoreBndr))
-> ([CoreBndr], Expr CoreBndr) -> ([CoreBndr], Expr CoreBndr)
forall a b. (a -> b) -> a -> b
$
      Bool -> Type -> Expr CoreBndr -> ([CoreBndr], Expr CoreBndr)
grabBody Bool
allowTC (Type -> Type
Ghc.expandTypeSynonyms Type
τ) (Expr CoreBndr -> ([CoreBndr], Expr CoreBndr))
-> Expr CoreBndr -> ([CoreBndr], Expr CoreBndr)
forall a b. (a -> b) -> a -> b
$
      Bool -> Expr CoreBndr -> Expr CoreBndr
normalizeCoreExpr Bool
allowTC Expr CoreBndr
def
    su :: SubstV Symbol
su         = [(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst  ([(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol)
-> [(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol
forall a b. (a -> b) -> a -> b
$ [Symbol]
-> [ExprBV Symbol Symbol] -> [(Symbol, ExprBV Symbol Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip (CoreBndr -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol     (CoreBndr -> Symbol) -> [CoreBndr] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CoreBndr]
xs) [ExprBV Symbol Symbol]
forall {b}. [ExprBV b Symbol]
xArgs
                           [(Symbol, ExprBV Symbol Symbol)]
-> [(Symbol, ExprBV Symbol Symbol)]
-> [(Symbol, ExprBV Symbol Symbol)]
forall a. [a] -> [a] -> [a]
++ [Symbol]
-> [ExprBV Symbol Symbol] -> [(Symbol, ExprBV Symbol Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip (CoreBndr -> Symbol
forall t. NamedThing t => t -> Symbol
simplesymbol (CoreBndr -> Symbol) -> [CoreBndr] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CoreBndr]
xs) [ExprBV Symbol Symbol]
forall {b}. [ExprBV b Symbol]
xArgs
    xts :: [(Symbol, Sort)]
xts        = [(Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Symbol
x, TCEmb TyCon -> RType RTyCon RTyVar RReft -> Sort
rTypeSortExp TCEmb TyCon
tce RType RTyCon RTyVar RReft
t) | (Symbol
x, RType RTyCon RTyVar RReft
t) <- AxiomType -> [(Symbol, RType RTyCon RTyVar RReft)]
aargs AxiomType
at]

rTypeSortExp :: F.TCEmb Ghc.TyCon -> SpecType -> F.Sort
rTypeSortExp :: TCEmb TyCon -> RType RTyCon RTyVar RReft -> Sort
rTypeSortExp TCEmb TyCon
tce = TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce (Type -> Sort)
-> (RType RTyCon RTyVar RReft -> Type)
-> RType RTyCon RTyVar RReft
-> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
Ghc.expandTypeSynonyms (Type -> Type)
-> (RType RTyCon RTyVar RReft -> Type)
-> RType RTyCon RTyVar RReft
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> RType RTyCon RTyVar RReft -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False

grabBody :: Bool -- ^ typeclass enabled
         -> Ghc.Type -> Ghc.CoreExpr -> ([Ghc.Var], Ghc.CoreExpr)
grabBody :: Bool -> Type -> Expr CoreBndr -> ([CoreBndr], Expr CoreBndr)
grabBody Bool
allowTC (Ghc.ForAllTy ForAllTyBinder
_ Type
ty) Expr CoreBndr
e
  = Bool -> Type -> Expr CoreBndr -> ([CoreBndr], Expr CoreBndr)
grabBody Bool
allowTC Type
ty Expr CoreBndr
e
grabBody allowTC :: Bool
allowTC@Bool
False Ghc.FunTy{ ft_arg :: Type -> Type
Ghc.ft_arg = Type
tx, ft_res :: Type -> Type
Ghc.ft_res = Type
t} Expr CoreBndr
e | Type -> Bool
Ghc.isClassPred Type
tx
  = Bool -> Type -> Expr CoreBndr -> ([CoreBndr], Expr CoreBndr)
grabBody Bool
allowTC Type
t Expr CoreBndr
e
grabBody allowTC :: Bool
allowTC@Bool
True Ghc.FunTy{ ft_arg :: Type -> Type
Ghc.ft_arg = Type
tx, ft_res :: Type -> Type
Ghc.ft_res = Type
t} Expr CoreBndr
e | Type -> Bool
isEmbeddedDictType Type
tx
  = Bool -> Type -> Expr CoreBndr -> ([CoreBndr], Expr CoreBndr)
grabBody Bool
allowTC Type
t Expr CoreBndr
e
grabBody Bool
allowTC torig :: Type
torig@Ghc.FunTy {} (Ghc.Let (Ghc.NonRec CoreBndr
x Expr CoreBndr
e) Expr CoreBndr
body)
  = Bool -> Type -> Expr CoreBndr -> ([CoreBndr], Expr CoreBndr)
grabBody Bool
allowTC Type
torig ((CoreBndr, Expr CoreBndr) -> Expr CoreBndr -> Expr CoreBndr
forall a. Subable a => (CoreBndr, Expr CoreBndr) -> a -> a
subst (CoreBndr
x,Expr CoreBndr
e) Expr CoreBndr
body)
grabBody Bool
allowTC Ghc.FunTy{ ft_res :: Type -> Type
Ghc.ft_res = Type
t} (Ghc.Lam CoreBndr
x Expr CoreBndr
e)
  = (CoreBndr
xCoreBndr -> [CoreBndr] -> [CoreBndr]
forall a. a -> [a] -> [a]
:[CoreBndr]
xs, Expr CoreBndr
e') where ([CoreBndr]
xs, Expr CoreBndr
e') = Bool -> Type -> Expr CoreBndr -> ([CoreBndr], Expr CoreBndr)
grabBody Bool
allowTC Type
t Expr CoreBndr
e
grabBody Bool
allowTC Type
t (Ghc.Tick CoreTickish
_ Expr CoreBndr
e)
  = Bool -> Type -> Expr CoreBndr -> ([CoreBndr], Expr CoreBndr)
grabBody Bool
allowTC Type
t Expr CoreBndr
e
grabBody Bool
allowTC ty :: Type
ty@Ghc.FunTy{} Expr CoreBndr
e
  = ([CoreBndr]
txs[CoreBndr] -> [CoreBndr] -> [CoreBndr]
forall a. [a] -> [a] -> [a]
++[CoreBndr]
xs, Expr CoreBndr
e')
   where ([Type]
ts,Type
tr)  = Type -> ([Type], Type)
splitFun Type
ty
         ([CoreBndr]
xs, Expr CoreBndr
e') = Bool -> Type -> Expr CoreBndr -> ([CoreBndr], Expr CoreBndr)
grabBody Bool
allowTC Type
tr ((Expr CoreBndr -> Expr CoreBndr -> Expr CoreBndr)
-> Expr CoreBndr -> [Expr CoreBndr] -> Expr CoreBndr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr CoreBndr -> Expr CoreBndr -> Expr CoreBndr
forall b. Expr b -> Expr b -> Expr b
Ghc.App Expr CoreBndr
e (CoreBndr -> Expr CoreBndr
forall b. CoreBndr -> Expr b
Ghc.Var (CoreBndr -> Expr CoreBndr) -> [CoreBndr] -> [Expr CoreBndr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CoreBndr]
txs))
         txs :: [CoreBndr]
txs      = [ [Char] -> Type -> CoreBndr
stringVar ([Char]
"ls" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i) Type
t |  (Type
t,Int
i) <- [Type] -> [Int] -> [(Type, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
ts [(Int
1::Int)..]]
grabBody Bool
_ Type
_ Expr CoreBndr
e
  = ([], Expr CoreBndr
e)

splitFun :: Ghc.Type -> ([Ghc.Type], Ghc.Type)
splitFun :: Type -> ([Type], Type)
splitFun = [Type] -> Type -> ([Type], Type)
go []
  where go :: [Type] -> Type -> ([Type], Type)
go [Type]
acc Ghc.FunTy{ ft_arg :: Type -> Type
Ghc.ft_arg = Type
tx, ft_res :: Type -> Type
Ghc.ft_res = Type
t} = [Type] -> Type -> ([Type], Type)
go (Type
txType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
acc) Type
t
        go [Type]
acc Type
t                                           = ([Type] -> [Type]
forall a. [a] -> [a]
reverse [Type]
acc, Type
t)


isBoolBind :: Ghc.Var -> Bool
isBoolBind :: InterestingVarFun
isBoolBind CoreBndr
v = RType RTyCon RTyVar () -> Bool
forall t t1. RType RTyCon t t1 -> Bool
isBool (RTypeRepBV Symbol Symbol RTyCon RTyVar () -> RType RTyCon RTyVar ()
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
ty_res (RTypeRepBV Symbol Symbol RTyCon RTyVar ()
 -> RType RTyCon RTyVar ())
-> RTypeRepBV Symbol Symbol RTyCon RTyVar ()
-> RType RTyCon RTyVar ()
forall a b. (a -> b) -> a -> b
$ RType RTyCon RTyVar () -> RTypeRepBV Symbol Symbol RTyCon RTyVar ()
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep ((Type -> RType RTyCon RTyVar ()
forall r. IsReft r => Type -> RRType r
ofType (Type -> RType RTyCon RTyVar ()) -> Type -> RType RTyCon RTyVar ()
forall a b. (a -> b) -> a -> b
$ CoreBndr -> Type
Ghc.varType CoreBndr
v) :: RRType ()))

strengthenRes :: SpecType -> F.Reft -> SpecType
strengthenRes :: RType RTyCon RTyVar RReft
-> ReftBV Symbol Symbol -> RType RTyCon RTyVar RReft
strengthenRes RType RTyCon RTyVar RReft
st ReftBV Symbol Symbol
rf = RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall {r} {b} {v} {c} {tv}.
(ReftBind r ~ Symbol, ReftVar r ~ Symbol, IsReft r) =>
RTypeBV b v c tv r -> RTypeBV b v c tv r
go RType RTyCon RTyVar RReft
st
  where
    go :: RTypeBV b v c tv r -> RTypeBV b v c tv r
go (RAllT RTVUBV b v c tv
a RTypeBV b v c tv r
t r
r)   = RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
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 b v c tv
a (RTypeBV b v c tv r -> RTypeBV b v c tv r
go RTypeBV b v c tv r
t) r
r
    go (RAllP PVUBV b v c tv
p RTypeBV b v c tv r
t)     = PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
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 b v c tv
p (RTypeBV b v c tv r -> RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
forall a b. (a -> b) -> a -> b
$ RTypeBV b v c tv r -> RTypeBV b v c tv r
go RTypeBV b v c tv r
t
    go (RFun b
x RFInfo
i RTypeBV b v c tv r
tx RTypeBV b v c tv r
t r
r) = b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
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 b
x RFInfo
i RTypeBV b v c tv r
tx (RTypeBV b v c tv r -> RTypeBV b v c tv r
go RTypeBV b v c tv r
t) r
r
    go RTypeBV b v c tv r
t               =  RTypeBV b v c tv r
t RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
`strengthen` ReftBV (ReftBind r) (ReftVar r) -> r
forall r. IsReft r => ReftBV (ReftBind r) (ReftVar r) -> r
ofReft ReftBV Symbol Symbol
ReftBV (ReftBind r) (ReftVar r)
rf

class Subable a where
  subst :: (Ghc.Var, Ghc.CoreExpr) -> a -> a

instance Subable Ghc.Var where
  subst :: (CoreBndr, Expr CoreBndr) -> CoreBndr -> CoreBndr
subst (CoreBndr
x, Expr CoreBndr
ex) CoreBndr
z
    | CoreBndr
x CoreBndr -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
== CoreBndr
z, Ghc.Var CoreBndr
y <- Expr CoreBndr
ex = CoreBndr
y
    | Bool
otherwise           = CoreBndr
z

instance Subable Ghc.CoreExpr where
  subst :: (CoreBndr, Expr CoreBndr) -> Expr CoreBndr -> Expr CoreBndr
subst (CoreBndr
x, Expr CoreBndr
ex) (Ghc.Var CoreBndr
y)
    | CoreBndr
x CoreBndr -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
== CoreBndr
y    = Expr CoreBndr
ex
    | Bool
otherwise = CoreBndr -> Expr CoreBndr
forall b. CoreBndr -> Expr b
Ghc.Var CoreBndr
y
  subst (CoreBndr, Expr CoreBndr)
su (Ghc.App Expr CoreBndr
f Expr CoreBndr
e)
    = Expr CoreBndr -> Expr CoreBndr -> Expr CoreBndr
forall b. Expr b -> Expr b -> Expr b
Ghc.App ((CoreBndr, Expr CoreBndr) -> Expr CoreBndr -> Expr CoreBndr
forall a. Subable a => (CoreBndr, Expr CoreBndr) -> a -> a
subst (CoreBndr, Expr CoreBndr)
su Expr CoreBndr
f) ((CoreBndr, Expr CoreBndr) -> Expr CoreBndr -> Expr CoreBndr
forall a. Subable a => (CoreBndr, Expr CoreBndr) -> a -> a
subst (CoreBndr, Expr CoreBndr)
su Expr CoreBndr
e)
  subst (CoreBndr, Expr CoreBndr)
su (Ghc.Lam CoreBndr
x Expr CoreBndr
e)
    = CoreBndr -> Expr CoreBndr -> Expr CoreBndr
forall b. b -> Expr b -> Expr b
Ghc.Lam CoreBndr
x ((CoreBndr, Expr CoreBndr) -> Expr CoreBndr -> Expr CoreBndr
forall a. Subable a => (CoreBndr, Expr CoreBndr) -> a -> a
subst (CoreBndr, Expr CoreBndr)
su Expr CoreBndr
e)
  subst (CoreBndr, Expr CoreBndr)
su (Ghc.Case Expr CoreBndr
e CoreBndr
x Type
t [Alt CoreBndr]
alts)
    = Expr CoreBndr
-> CoreBndr -> Type -> [Alt CoreBndr] -> Expr CoreBndr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Ghc.Case ((CoreBndr, Expr CoreBndr) -> Expr CoreBndr -> Expr CoreBndr
forall a. Subable a => (CoreBndr, Expr CoreBndr) -> a -> a
subst (CoreBndr, Expr CoreBndr)
su Expr CoreBndr
e) CoreBndr
x Type
t ((CoreBndr, Expr CoreBndr) -> Alt CoreBndr -> Alt CoreBndr
forall a. Subable a => (CoreBndr, Expr CoreBndr) -> a -> a
subst (CoreBndr, Expr CoreBndr)
su (Alt CoreBndr -> Alt CoreBndr) -> [Alt CoreBndr] -> [Alt CoreBndr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Alt CoreBndr]
alts)
  subst (CoreBndr, Expr CoreBndr)
su (Ghc.Let (Ghc.Rec [(CoreBndr, Expr CoreBndr)]
xes) Expr CoreBndr
e)
    = Bind CoreBndr -> Expr CoreBndr -> Expr CoreBndr
forall b. Bind b -> Expr b -> Expr b
Ghc.Let ([(CoreBndr, Expr CoreBndr)] -> Bind CoreBndr
forall b. [(b, Expr b)] -> Bind b
Ghc.Rec ((Expr CoreBndr -> Expr CoreBndr)
-> (CoreBndr, Expr CoreBndr) -> (CoreBndr, Expr CoreBndr)
forall a b. (a -> b) -> (CoreBndr, a) -> (CoreBndr, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((CoreBndr, Expr CoreBndr) -> Expr CoreBndr -> Expr CoreBndr
forall a. Subable a => (CoreBndr, Expr CoreBndr) -> a -> a
subst (CoreBndr, Expr CoreBndr)
su) ((CoreBndr, Expr CoreBndr) -> (CoreBndr, Expr CoreBndr))
-> [(CoreBndr, Expr CoreBndr)] -> [(CoreBndr, Expr CoreBndr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(CoreBndr, Expr CoreBndr)]
xes)) ((CoreBndr, Expr CoreBndr) -> Expr CoreBndr -> Expr CoreBndr
forall a. Subable a => (CoreBndr, Expr CoreBndr) -> a -> a
subst (CoreBndr, Expr CoreBndr)
su Expr CoreBndr
e)
  subst (CoreBndr, Expr CoreBndr)
su (Ghc.Let (Ghc.NonRec CoreBndr
x Expr CoreBndr
ex) Expr CoreBndr
e)
    = Bind CoreBndr -> Expr CoreBndr -> Expr CoreBndr
forall b. Bind b -> Expr b -> Expr b
Ghc.Let (CoreBndr -> Expr CoreBndr -> Bind CoreBndr
forall b. b -> Expr b -> Bind b
Ghc.NonRec CoreBndr
x ((CoreBndr, Expr CoreBndr) -> Expr CoreBndr -> Expr CoreBndr
forall a. Subable a => (CoreBndr, Expr CoreBndr) -> a -> a
subst (CoreBndr, Expr CoreBndr)
su Expr CoreBndr
ex)) ((CoreBndr, Expr CoreBndr) -> Expr CoreBndr -> Expr CoreBndr
forall a. Subable a => (CoreBndr, Expr CoreBndr) -> a -> a
subst (CoreBndr, Expr CoreBndr)
su Expr CoreBndr
e)
  subst (CoreBndr, Expr CoreBndr)
su (Ghc.Cast Expr CoreBndr
e CoercionR
t)
    = Expr CoreBndr -> CoercionR -> Expr CoreBndr
forall b. Expr b -> CoercionR -> Expr b
Ghc.Cast ((CoreBndr, Expr CoreBndr) -> Expr CoreBndr -> Expr CoreBndr
forall a. Subable a => (CoreBndr, Expr CoreBndr) -> a -> a
subst (CoreBndr, Expr CoreBndr)
su Expr CoreBndr
e) CoercionR
t
  subst (CoreBndr, Expr CoreBndr)
su (Ghc.Tick CoreTickish
t Expr CoreBndr
e)
    = CoreTickish -> Expr CoreBndr -> Expr CoreBndr
forall b. CoreTickish -> Expr b -> Expr b
Ghc.Tick CoreTickish
t ((CoreBndr, Expr CoreBndr) -> Expr CoreBndr -> Expr CoreBndr
forall a. Subable a => (CoreBndr, Expr CoreBndr) -> a -> a
subst (CoreBndr, Expr CoreBndr)
su Expr CoreBndr
e)
  subst (CoreBndr, Expr CoreBndr)
_ Expr CoreBndr
e
    = Expr CoreBndr
e

instance Subable Ghc.CoreAlt where
  subst :: (CoreBndr, Expr CoreBndr) -> Alt CoreBndr -> Alt CoreBndr
subst (CoreBndr, Expr CoreBndr)
su (Ghc.Alt AltCon
c [CoreBndr]
xs Expr CoreBndr
e) = AltCon -> [CoreBndr] -> Expr CoreBndr -> Alt CoreBndr
forall b. AltCon -> [b] -> Expr b -> Alt b
Ghc.Alt AltCon
c [CoreBndr]
xs ((CoreBndr, Expr CoreBndr) -> Expr CoreBndr -> Expr CoreBndr
forall a. Subable a => (CoreBndr, Expr CoreBndr) -> a -> a
subst (CoreBndr, Expr CoreBndr)
su Expr CoreBndr
e)

data AxiomType = AT { AxiomType -> RType RTyCon RTyVar RReft
aty :: SpecType, AxiomType -> [(Symbol, RType RTyCon RTyVar RReft)]
aargs :: [(F.Symbol, SpecType)], AxiomType -> RType RTyCon RTyVar RReft
ares :: SpecType }
  deriving Int -> AxiomType -> [Char] -> [Char]
[AxiomType] -> [Char] -> [Char]
AxiomType -> [Char]
(Int -> AxiomType -> [Char] -> [Char])
-> (AxiomType -> [Char])
-> ([AxiomType] -> [Char] -> [Char])
-> Show AxiomType
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> AxiomType -> [Char] -> [Char]
showsPrec :: Int -> AxiomType -> [Char] -> [Char]
$cshow :: AxiomType -> [Char]
show :: AxiomType -> [Char]
$cshowList :: [AxiomType] -> [Char] -> [Char]
showList :: [AxiomType] -> [Char] -> [Char]
Show

-- | Specification for Haskell function
--
-- @addSingletonApp allowTC f (x:_ -> y: -> {v:_ | p}@ produces a type
-- @x:_ -> y:_ -> {v:_ | p && v = f x y}@
--
addSingletonApp :: Bool -> F.Symbol -> SpecType -> AxiomType
addSingletonApp :: Bool -> Symbol -> RType RTyCon RTyVar RReft -> AxiomType
addSingletonApp Bool
allowTC Symbol
s RType RTyCon RTyVar RReft
st = RType RTyCon RTyVar RReft
-> [(Symbol, RType RTyCon RTyVar RReft)]
-> RType RTyCon RTyVar RReft
-> AxiomType
AT RType RTyCon RTyVar RReft
to ([(Symbol, RType RTyCon RTyVar RReft)]
-> [(Symbol, RType RTyCon RTyVar RReft)]
forall a. [a] -> [a]
reverse [(Symbol, RType RTyCon RTyVar RReft)]
xts) RType RTyCon RTyVar RReft
res
  where
    (RType RTyCon RTyVar RReft
to, (Int
_,[(Symbol, RType RTyCon RTyVar RReft)]
xts, Just RType RTyCon RTyVar RReft
res)) = State
  (Int, [(Symbol, RType RTyCon RTyVar RReft)],
   Maybe (RType RTyCon RTyVar RReft))
  (RType RTyCon RTyVar RReft)
-> (Int, [(Symbol, RType RTyCon RTyVar RReft)],
    Maybe (RType RTyCon RTyVar RReft))
-> (RType RTyCon RTyVar RReft,
    (Int, [(Symbol, RType RTyCon RTyVar RReft)],
     Maybe (RType RTyCon RTyVar RReft)))
forall s a. State s a -> s -> (a, s)
runState (RType RTyCon RTyVar RReft
-> State
     (Int, [(Symbol, RType RTyCon RTyVar RReft)],
      Maybe (RType RTyCon RTyVar RReft))
     (RType RTyCon RTyVar RReft)
forall {m :: * -> *} {v} {t}.
Monad m =>
RTypeBV Symbol v RTyCon t RReft
-> StateT
     (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
      Maybe (RTypeBV Symbol v RTyCon t RReft))
     m
     (RTypeBV Symbol v RTyCon t RReft)
go RType RTyCon RTyVar RReft
st) (Int
1,[], Maybe (RType RTyCon RTyVar RReft)
forall a. Maybe a
Nothing)
    go :: RTypeBV Symbol v RTyCon t RReft
-> StateT
     (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
      Maybe (RTypeBV Symbol v RTyCon t RReft))
     m
     (RTypeBV Symbol v RTyCon t RReft)
go (RAllT RTVUBV Symbol v RTyCon t
a RTypeBV Symbol v RTyCon t RReft
t RReft
r) = RTVUBV Symbol v RTyCon t
-> RTypeBV Symbol v RTyCon t RReft
-> RReft
-> RTypeBV Symbol v RTyCon t 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 v RTyCon t
a (RTypeBV Symbol v RTyCon t RReft
 -> RReft -> RTypeBV Symbol v RTyCon t RReft)
-> StateT
     (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
      Maybe (RTypeBV Symbol v RTyCon t RReft))
     m
     (RTypeBV Symbol v RTyCon t RReft)
-> StateT
     (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
      Maybe (RTypeBV Symbol v RTyCon t RReft))
     m
     (RReft -> RTypeBV Symbol v RTyCon t RReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeBV Symbol v RTyCon t RReft
-> StateT
     (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
      Maybe (RTypeBV Symbol v RTyCon t RReft))
     m
     (RTypeBV Symbol v RTyCon t RReft)
go RTypeBV Symbol v RTyCon t RReft
t StateT
  (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
   Maybe (RTypeBV Symbol v RTyCon t RReft))
  m
  (RReft -> RTypeBV Symbol v RTyCon t RReft)
-> StateT
     (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
      Maybe (RTypeBV Symbol v RTyCon t RReft))
     m
     RReft
-> StateT
     (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
      Maybe (RTypeBV Symbol v RTyCon t RReft))
     m
     (RTypeBV Symbol v RTyCon t RReft)
forall a b.
StateT
  (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
   Maybe (RTypeBV Symbol v RTyCon t RReft))
  m
  (a -> b)
-> StateT
     (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
      Maybe (RTypeBV Symbol v RTyCon t RReft))
     m
     a
-> StateT
     (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
      Maybe (RTypeBV Symbol v RTyCon t RReft))
     m
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RReft
-> StateT
     (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
      Maybe (RTypeBV Symbol v RTyCon t RReft))
     m
     RReft
forall a.
a
-> StateT
     (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
      Maybe (RTypeBV Symbol v RTyCon t RReft))
     m
     a
forall (m :: * -> *) a. Monad m => a -> m a
return RReft
r
    go (RAllP PVUBV Symbol v RTyCon t
p RTypeBV Symbol v RTyCon t RReft
t) = PVUBV Symbol v RTyCon t
-> RTypeBV Symbol v RTyCon t RReft
-> RTypeBV Symbol v RTyCon t 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 v RTyCon t
p (RTypeBV Symbol v RTyCon t RReft
 -> RTypeBV Symbol v RTyCon t RReft)
-> StateT
     (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
      Maybe (RTypeBV Symbol v RTyCon t RReft))
     m
     (RTypeBV Symbol v RTyCon t RReft)
-> StateT
     (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
      Maybe (RTypeBV Symbol v RTyCon t RReft))
     m
     (RTypeBV Symbol v RTyCon t RReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeBV Symbol v RTyCon t RReft
-> StateT
     (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
      Maybe (RTypeBV Symbol v RTyCon t RReft))
     m
     (RTypeBV Symbol v RTyCon t RReft)
go RTypeBV Symbol v RTyCon t RReft
t
    go (RFun Symbol
x RFInfo
i RTypeBV Symbol v RTyCon t RReft
tx RTypeBV Symbol v RTyCon t RReft
t RReft
r) | RTypeBV Symbol v RTyCon t RReft -> Bool
forall {v} {t} {t1}. RTypeV v RTyCon t t1 -> Bool
isErasable RTypeBV Symbol v RTyCon t RReft
tx = (\RTypeBV Symbol v RTyCon t RReft
t' -> Symbol
-> RFInfo
-> RTypeBV Symbol v RTyCon t RReft
-> RTypeBV Symbol v RTyCon t RReft
-> RReft
-> RTypeBV Symbol v RTyCon t 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
x RFInfo
i RTypeBV Symbol v RTyCon t RReft
tx RTypeBV Symbol v RTyCon t RReft
t' RReft
r) (RTypeBV Symbol v RTyCon t RReft
 -> RTypeBV Symbol v RTyCon t RReft)
-> StateT
     (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
      Maybe (RTypeBV Symbol v RTyCon t RReft))
     m
     (RTypeBV Symbol v RTyCon t RReft)
-> StateT
     (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
      Maybe (RTypeBV Symbol v RTyCon t RReft))
     m
     (RTypeBV Symbol v RTyCon t RReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeBV Symbol v RTyCon t RReft
-> StateT
     (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
      Maybe (RTypeBV Symbol v RTyCon t RReft))
     m
     (RTypeBV Symbol v RTyCon t RReft)
go RTypeBV Symbol v RTyCon t RReft
t
    go (RFun Symbol
x RFInfo
ii RTypeBV Symbol v RTyCon t RReft
tx RTypeBV Symbol v RTyCon t RReft
t RReft
r) = do
      (i,bs,mres) <- StateT
  (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
   Maybe (RTypeBV Symbol v RTyCon t RReft))
  m
  (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
   Maybe (RTypeBV Symbol v RTyCon t RReft))
forall (m :: * -> *) s. Monad m => StateT s m s
get
      let x' = Symbol -> Int -> Symbol
unDummy Symbol
x Int
i
      put (i+1, (x', tx):bs,mres)
      t' <- go t
      return $ RFun x' ii tx t' r
    go RTypeBV Symbol v RTyCon t RReft
t = do
      (i,bs,_) <- StateT
  (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
   Maybe (RTypeBV Symbol v RTyCon t RReft))
  m
  (Int, [(Symbol, RTypeBV Symbol v RTyCon t RReft)],
   Maybe (RTypeBV Symbol v RTyCon t RReft))
forall (m :: * -> *) s. Monad m => StateT s m s
get
      let ys = [Symbol] -> [Symbol]
forall a. [a] -> [a]
reverse ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ ((Symbol, RTypeBV Symbol v RTyCon t RReft) -> Symbol)
-> [(Symbol, RTypeBV Symbol v RTyCon t RReft)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, RTypeBV Symbol v RTyCon t RReft) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, RTypeBV Symbol v RTyCon t RReft)]
bs
      let t' = RTypeBV Symbol v RTyCon t RReft
-> RReft -> RTypeBV Symbol v RTyCon t RReft
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
strengthen RTypeBV Symbol v RTyCon t RReft
t (Symbol -> [Symbol] -> RReft
forall a. Symbolic a => Symbol -> [a] -> RReft
singletonApp Symbol
s [Symbol]
ys)
      put (i, bs, Just t')
      return t'
    isErasable :: RTypeV v RTyCon t t1 -> Bool
isErasable = if Bool
allowTC then RTypeV v RTyCon t t1 -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isEmbeddedClass else RTypeV v RTyCon t t1 -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType
unDummy :: F.Symbol -> Int -> F.Symbol
unDummy :: Symbol -> Int -> Symbol
unDummy Symbol
x Int
i
  | Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= Symbol
F.dummySymbol = Symbol
x
  | Bool
otherwise          = [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Char]
"lq" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i)

singletonApp :: F.Symbolic a => F.Symbol -> [a] -> UReft F.Reft
singletonApp :: forall a. Symbolic a => Symbol -> [a] -> RReft
singletonApp Symbol
s [a]
ys = ReftBV Symbol Symbol -> PredicateBV Symbol Symbol -> RReft
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ReftBV Symbol Symbol
r PredicateBV Symbol Symbol
forall a. Monoid a => a
mempty
  where
    r :: ReftBV Symbol Symbol
r             = ExprBV Symbol Symbol -> ReftBV Symbol Symbol
forall a. Expression a => a -> ReftBV Symbol Symbol
F.exprReft (ExprBV Symbol Symbol
-> [ExprBV Symbol Symbol] -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> [ExprBV b v] -> ExprBV b v
F.eApps (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
s) (a -> ExprBV Symbol Symbol
forall a. Symbolic a => a -> ExprBV Symbol Symbol
F.eVar (a -> ExprBV Symbol Symbol) -> [a] -> [ExprBV Symbol Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
ys))