{-# 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

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 [(Id, LocSpecType, Equation)]
makeHaskellAxioms GhcSrc
src Env
env TycEnv
tycEnv LogicMap
lmap GhcSpecSig
spSig BareSpec
spec = do
  let refDefs :: [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
refDefs = GhcSrc
-> GhcSpecSig
-> BareSpec
-> Env
-> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
getReflectDefs GhcSrc
src GhcSpecSig
spSig BareSpec
spec Env
env
  [(Id, LocSpecType, Equation)]
-> Lookup [(Id, LocSpecType, Equation)]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
-> TycEnv
-> LogicMap
-> (LocSymbol, Maybe SpecType, Id, CoreExpr)
-> (Id, LocSpecType, Equation)
makeAxiom Env
env TycEnv
tycEnv LogicMap
lmap ((LocSymbol, Maybe SpecType, Id, CoreExpr)
 -> (Id, LocSpecType, Equation))
-> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
-> [(Id, LocSpecType, Equation)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
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 [(Id, 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 [(Id, LocSpecType, Equation)]
forall a e. (?callStack::CallStack, Exception e) => e -> a
Ex.throw (Error -> Lookup [(Id, LocSpecType, Equation)])
-> Error -> Lookup [(Id, 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]
++
                      LocSymbol -> [Char]
forall a. Show a => a -> [Char]
show ((?callStack::CallStack) => LHName -> Symbol
LHName -> Symbol
lhNameToUnqualifiedSymbol (LHName -> Symbol) -> Located LHName -> LocSymbol
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]
++
                      LocSymbol -> [Char]
forall a. Show a => a -> [Char]
show ((?callStack::CallStack) => LHName -> Symbol
LHName -> Symbol
lhNameToUnqualifiedSymbol (LHName -> Symbol) -> Located LHName -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located LHName
y)
    Maybe (Located LHName, Located LHName)
Nothing -> [(Id, LocSpecType, Equation)]
-> Lookup [(Id, LocSpecType, Equation)]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Id, LocSpecType, Equation)]
 -> Lookup [(Id, LocSpecType, Equation)])
-> [(Id, LocSpecType, Equation)]
-> Lookup [(Id, LocSpecType, Equation)]
forall a b. (a -> b) -> a -> b
$ (Located LHName, Located LHName) -> (Id, LocSpecType, Equation)
turnIntoAxiom ((Located LHName, Located LHName) -> (Id, LocSpecType, Equation))
-> [(Located LHName, Located LHName)]
-> [(Id, 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) -> (Id, LocSpecType, Equation)
turnIntoAxiom (Located LHName
actual, Located LHName
pretended) = GhcSpecSig
-> Env
-> TCEmb TyCon
-> (Located LHName, Located LHName)
-> (Id, LocSpecType, Equation)
makeAssumeReflectAxiom GhcSpecSig
spSig Env
env TCEmb TyCon
embs (Located LHName
actual, Located LHName
pretended)
    refDefs :: [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
refDefs                 = GhcSrc
-> GhcSpecSig
-> BareSpec
-> Env
-> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
getReflectDefs GhcSrc
src GhcSpecSig
spSig BareSpec
spec Env
env
    embs :: TCEmb TyCon
embs                    = TycEnv -> TCEmb TyCon
Bare.tcEmbs       TycEnv
tycEnv
    refSymbols :: [Located LHName]
refSymbols              =
      (\(LocSymbol
x, Maybe SpecType
_, Id
v, CoreExpr
_) -> LocSymbol -> LHName -> Located LHName
forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
x (LHName -> Located LHName) -> LHName -> Located LHName
forall a b. (a -> b) -> a -> b
$ Name -> Symbol -> LHName
makeGHCLHName (Id -> Name
forall a. NamedThing a => a -> Name
Ghc.getName Id
v) (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
v)) ((LocSymbol, Maybe SpecType, Id, CoreExpr) -> Located LHName)
-> [(LocSymbol, Maybe SpecType, Id, CoreExpr)] -> [Located LHName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
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)
-> (Id, 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 Kind
pretendedTy Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
actualTy then
    (Id
actualV, Located LHName
actual{val = aty at}, Equation
actualEq)
  else
    Error -> (Id, LocSpecType, Equation)
forall a e. (?callStack::CallStack, Exception e) => e -> a
Ex.throw (Error -> (Id, LocSpecType, Equation))
-> Error -> (Id, 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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Kind -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp Kind
pretendedTy [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" and " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Kind -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp Kind
actualTy  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" do not match."
  where
    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 -> Id -> LocSymbol -> Located AxiomType
strengthenSpecWithMeasure GhcSpecSig
sig Env
env Id
actualV Located LHName
pretended{val=qPretended}

    -- Get the Ghc.Var's of the actual and pretended function names
    actualV :: Id
actualV = case (?callStack::CallStack) => Env -> Located LHName -> Lookup Id
Env -> Located LHName -> Lookup Id
Bare.lookupGhcIdLHName Env
env Located LHName
actual of
      Right Id
x -> Id
x
      Left [Error]
_ -> Maybe SrcSpan -> [Char] -> Id
forall a. (?callStack::CallStack) => 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 :: Id
pretendedV = case (?callStack::CallStack) => Env -> Located LHName -> Lookup Id
Env -> Located LHName -> Lookup Id
Bare.lookupGhcIdLHName Env
env Located LHName
pretended of
      Right Id
x -> Id
x
      Left [Error]
_ -> Maybe SrcSpan -> [Char] -> Id
forall a. (?callStack::CallStack) => 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. (?callStack::CallStack) => 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 :: Kind
actualTy = Id -> Kind
Ghc.varType Id
actualV
    pretendedTy :: Kind
pretendedTy = Id -> Kind
Ghc.varType Id
pretendedV

    -- The return type of the function
    out :: Sort
out   = TCEmb TyCon -> SpecType -> Sort
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RRType ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce (SpecType -> Sort) -> SpecType -> Sort
forall a b. (a -> b) -> a -> b
$ AxiomType -> SpecType
ares AxiomType
at
    -- The arguments names and types, as given by `AxiomType`
    xArgs :: [(Symbol, Sort)]
xArgs = (SpecType -> Sort) -> (Symbol, SpecType) -> (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 -> SpecType -> Sort
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RRType ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce) ((Symbol, SpecType) -> (Symbol, Sort))
-> [(Symbol, SpecType)] -> [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AxiomType -> [(Symbol, SpecType)]
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 :: Expr
le    = (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
F.EApp (Symbol -> Expr
forall v. v -> ExprV v
F.EVar Symbol
qPretended) (Symbol -> Expr
forall v. v -> ExprV v
F.EVar (Symbol -> Expr)
-> ((Symbol, Sort) -> Symbol) -> (Symbol, Sort) -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Sort) -> Expr) -> [(Symbol, Sort)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
xArgs)

    actualEq :: Equation
actualEq = Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
F.mkEquation Symbol
qActual [(Symbol, Sort)]
xArgs Expr
le Sort
out

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

    -- Compute the refined type of the actual function. See `makeAssumeType` for details
    sigs :: [(Id, LocSpecType)]
sigs                    = GhcSpecSig -> [(Id, LocSpecType)]
gsTySigs GhcSpecSig
sig [(Id, LocSpecType)] -> [(Id, LocSpecType)] -> [(Id, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Id, LocSpecType)]
gsAsmSigs GhcSpecSig
sig -- We also look into assumed signatures
    -- Try to get the specification of the actual function from the signatures
    mbT :: Maybe SpecType
mbT   = LocSpecType -> SpecType
forall a. Located a -> a
val (LocSpecType -> SpecType) -> Maybe LocSpecType -> Maybe SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Id -> [(Id, LocSpecType)] -> Maybe LocSpecType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Id
actualV [(Id, 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 :: SpecType
rt    = RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
fromRTypeRep (RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType)
-> (SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft)
-> SpecType
-> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            (\trep :: RTypeRepV Symbol RTyCon RTyVar RReft
trep@RTypeRep{[(RTVar RTyVar (RRType ()), RReft)]
[Symbol]
[RReft]
[SpecType]
[PVarV Symbol (RRType ())]
[RFInfo]
SpecType
ty_vars :: [(RTVar RTyVar (RRType ()), RReft)]
ty_preds :: [PVarV Symbol (RRType ())]
ty_binds :: [Symbol]
ty_info :: [RFInfo]
ty_refts :: [RReft]
ty_args :: [SpecType]
ty_res :: SpecType
ty_res :: forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_args :: forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_refts :: forall v c tv r. RTypeRepV v c tv r -> [r]
ty_info :: forall v c tv r. RTypeRepV v c tv r -> [RFInfo]
ty_binds :: forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_preds :: forall v c tv r. RTypeRepV v c tv r -> [PVarV v (RTypeV v c tv ())]
ty_vars :: forall v c tv r.
RTypeRepV v c tv r -> [(RTVar tv (RTypeV v c tv ()), r)]
..} ->
                RTypeRepV Symbol RTyCon RTyVar RReft
trep{ty_info = fmap (\RFInfo
i -> RFInfo
i{permitTC = Just allowTC}) ty_info}) (RTypeRepV Symbol RTyCon RTyVar RReft
 -> RTypeRepV Symbol RTyCon RTyVar RReft)
-> (SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft)
-> SpecType
-> RTypeRepV Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ SpecType -> Maybe SpecType -> SpecType
forall a. a -> Maybe a -> a
Mb.fromMaybe (Kind -> SpecType
forall r. Monoid r => Kind -> RRType r
ofType Kind
actualTy) Maybe SpecType
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
-> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
getReflectDefs GhcSrc
src GhcSpecSig
sig BareSpec
spec Env
env =
  [ToReflectName]
-> HashMap LocSymbol Id
-> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
-> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
searchInTransitiveClosure [ToReflectName]
symsToResolve HashMap LocSymbol Id
forall {k} {v}. HashMap k v
initialDefinedMap []
  where
    sigs :: [(Id, LocSpecType)]
sigs                    = GhcSpecSig -> [(Id, LocSpecType)]
gsTySigs GhcSpecSig
sig
    symsToResolve :: [ToReflectName]
symsToResolve =
      (Located LHName -> ToReflectName)
-> [Located LHName] -> [ToReflectName]
forall a b. (a -> b) -> [a] -> [b]
map Located LHName -> ToReflectName
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)) [ToReflectName] -> [ToReflectName] -> [ToReflectName]
forall a. [a] -> [a] -> [a]
++
      (LocSymbol -> ToReflectName) -> [LocSymbol] -> [ToReflectName]
forall a b. (a -> b) -> [a] -> [b]
map LocSymbol -> ToReflectName
forall a b. b -> Either a b
Right (HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList (BareSpec -> HashSet LocSymbol
forall lname ty. Spec lname ty -> HashSet LocSymbol
Ms.privateReflects BareSpec
spec))
    cbs :: [(Id, CoreExpr)]
cbs = [Bind Id] -> [(Id, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
Ghc.flattenBinds ([Bind Id] -> [(Id, CoreExpr)]) -> [Bind Id] -> [(Id, CoreExpr)]
forall a b. (a -> b) -> a -> b
$ GhcSrc -> [Bind Id]
_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 :: [ToReflectName]
-> HashMap LocSymbol Id
-> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
-> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
searchInTransitiveClosure [] HashMap LocSymbol Id
_ [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
acc = [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
acc
    -- Recursive case: there are some left.
    searchInTransitiveClosure [ToReflectName]
toResolve HashMap LocSymbol Id
fvMap [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
acc = if [(LocSymbol, Maybe SpecType, Id, CoreExpr)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
found
         then case [ToReflectName]
newToResolve of
                -- No one newly found but no one left to process - we're good
                [] -> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
acc
                -- No one newly found but at least one symbol left - we throw
                -- an error
                ToReflectName
x:[ToReflectName]
_ -> Error -> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
forall a e. (?callStack::CallStack, Exception e) => e -> a
Ex.throw (Error -> [(LocSymbol, Maybe SpecType, Id, CoreExpr)])
-> ([Char] -> Error)
-> [Char]
-> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located LHName -> [Char] -> Error)
-> (LocSymbol -> [Char] -> Error)
-> ToReflectName
-> [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 LocSymbol -> [Char] -> Error
forall a. PPrint a => Located a -> [Char] -> Error
mkError ToReflectName
x ([Char] -> [(LocSymbol, Maybe SpecType, Id, CoreExpr)])
-> [Char] -> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
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]
++
                    (Id -> [Char] -> [Char])
-> [Char] -> HashMap LocSymbol Id -> [Char]
forall a b. (a -> b -> b) -> b -> HashMap LocSymbol a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Id
x1 [Char]
acc1 -> [Char]
acc1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" , " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Id -> [Char]
forall a. Show a => a -> [Char]
show Id
x1) [Char]
"" HashMap LocSymbol Id
newFvMap
         else [ToReflectName]
-> HashMap LocSymbol Id
-> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
-> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
searchInTransitiveClosure [ToReflectName]
newToResolve HashMap LocSymbol Id
newFvMap [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
newAcc
      where
        -- Try to get the definitions of the symbols that are left (`toResolve`)
        resolvedSyms :: [Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr)]
resolvedSyms = [(Id, CoreExpr)]
-> [(Id, LocSpecType)]
-> Env
-> HashMap LocSymbol Id
-> ToReflectName
-> Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr)
findVarDefType [(Id, CoreExpr)]
cbs [(Id, LocSpecType)]
sigs Env
env HashMap LocSymbol Id
fvMap (ToReflectName -> Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr))
-> [ToReflectName]
-> [Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ToReflectName]
toResolve
        -- Collect the newly found definitions
        found :: [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
found     = [Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr)]
-> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
forall a. [Maybe a] -> [a]
Mb.catMaybes [Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr)]
resolvedSyms
        -- Add them to the accumulator
        newAcc :: [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
newAcc    = [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
acc [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
-> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
-> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
forall a. [a] -> [a] -> [a]
++ [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
found
        -- Add any variable occurrence in them to `fvMap`
        newFvMap :: HashMap LocSymbol Id
newFvMap = (HashMap LocSymbol Id
 -> (LocSymbol, Maybe SpecType, Id, CoreExpr)
 -> HashMap LocSymbol Id)
-> HashMap LocSymbol Id
-> [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
-> HashMap LocSymbol Id
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl HashMap LocSymbol Id
-> (LocSymbol, Maybe SpecType, Id, CoreExpr)
-> HashMap LocSymbol Id
forall {a} {b} {c}.
HashMap LocSymbol Id -> (a, b, c, CoreExpr) -> HashMap LocSymbol Id
addFreeVarsToMap HashMap LocSymbol Id
fvMap [(LocSymbol, Maybe SpecType, Id, CoreExpr)]
found
        -- Collect all the symbols that still failed to be resolved in this
        -- iteration
        newToResolve :: [ToReflectName]
newToResolve = [ToReflectName
x | (ToReflectName
x, Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr)
Nothing) <- [ToReflectName]
-> [Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr)]
-> [(ToReflectName,
     Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr))]
forall a b. [a] -> [b] -> [(a, b)]
zip [ToReflectName]
toResolve [Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr)]
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 LocSymbol Id -> (a, b, c, CoreExpr) -> HashMap LocSymbol Id
addFreeVarsToMap HashMap LocSymbol Id
fvMap (a
_, b
_, c
_, CoreExpr
expr) =
      let freeVarsSet :: [Id]
freeVarsSet = CoreExpr -> [Id]
getAllFreeVars CoreExpr
expr
          newVars :: HashMap LocSymbol Id
newVars =
            [(LocSymbol, Id)] -> HashMap LocSymbol Id
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Id -> LocSymbol
Bare.varLocSym Id
var, Id
var) | Id
var <- [Id]
freeVarsSet]
      in HashMap LocSymbol Id
-> HashMap LocSymbol Id -> HashMap LocSymbol Id
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
M.union HashMap LocSymbol Id
fvMap HashMap LocSymbol Id
newVars

    getAllFreeVars :: CoreExpr -> [Id]
getAllFreeVars = InterestingVarFun -> CoreExpr -> [Id]
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 :: [(Id, CoreExpr)]
-> [(Id, LocSpecType)]
-> Env
-> HashMap LocSymbol Id
-> ToReflectName
-> Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr)
findVarDefType [(Id, CoreExpr)]
cbs [(Id, LocSpecType)]
sigs Env
env HashMap LocSymbol Id
_defs (Left Located LHName
x) =
  case ((Id, CoreExpr) -> Bool)
-> [(Id, CoreExpr)] -> Maybe (Id, CoreExpr)
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)
-> ((Id, CoreExpr) -> LHName) -> (Id, CoreExpr) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> LHName
makeGHCLHNameFromId (Id -> LHName)
-> ((Id, CoreExpr) -> Id) -> (Id, CoreExpr) -> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, CoreExpr) -> Id
forall a b. (a, b) -> a
fst) [(Id, CoreExpr)]
cbs of
  -- YL: probably ok even without checking typeclass flag since user cannot
  -- manually reflect internal names
  Just (Id
v, CoreExpr
e) ->
    (LocSymbol, Maybe SpecType, Id, CoreExpr)
-> Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr)
forall a. a -> Maybe a
Just ((LHName -> Symbol) -> Located LHName -> LocSymbol
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 -> SpecType
forall a. Located a -> a
val (LocSpecType -> SpecType) -> Maybe LocSpecType -> Maybe SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Id -> [(Id, LocSpecType)] -> Maybe LocSpecType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Id
v [(Id, LocSpecType)]
sigs, Id
v, CoreExpr
e)
  Maybe (Id, CoreExpr)
Nothing     -> do
    let ecall :: a
ecall = Maybe SrcSpan -> [Char] -> a
forall a. (?callStack::CallStack) => 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 :: Id
var = ([Error] -> Id) -> (Id -> Id) -> Lookup Id -> Id
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either [Error] -> Id
forall {a}. a
ecall Id -> Id
forall a. a -> a
id ((?callStack::CallStack) => Env -> Located LHName -> Lookup Id
Env -> Located LHName -> Lookup Id
Bare.lookupGhcIdLHName Env
env Located LHName
x)
        info :: IdInfo
info = HasDebugCallStack => Id -> IdInfo
Id -> IdInfo
Ghc.idInfo Id
var
        unfolding :: Maybe CoreExpr
unfolding = Unfolding -> Maybe CoreExpr
getExprFromUnfolding (Unfolding -> Maybe CoreExpr)
-> (IdInfo -> Unfolding) -> IdInfo -> Maybe CoreExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IdInfo -> Unfolding
Ghc.realUnfoldingInfo (IdInfo -> Maybe CoreExpr) -> IdInfo -> Maybe CoreExpr
forall a b. (a -> b) -> a -> b
$ IdInfo
info
    case Maybe CoreExpr
unfolding of
      Just CoreExpr
e ->
        (LocSymbol, Maybe SpecType, Id, CoreExpr)
-> Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr)
forall a. a -> Maybe a
Just ((LHName -> Symbol) -> Located LHName -> LocSymbol
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 -> SpecType
forall a. Located a -> a
val (LocSpecType -> SpecType) -> Maybe LocSpecType -> Maybe SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Id -> [(Id, LocSpecType)] -> Maybe LocSpecType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Id
var [(Id, LocSpecType)]
sigs, Id
var, CoreExpr
e)
      Maybe CoreExpr
_ ->
        Error -> Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr)
forall a e. (?callStack::CallStack, Exception e) => e -> a
Ex.throw (Error -> Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr))
-> Error -> Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr)
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 [(Id, CoreExpr)]
_cbs [(Id, LocSpecType)]
sigs Env
_env HashMap LocSymbol Id
defs (Right LocSymbol
x) = do
    var <- LocSymbol -> HashMap LocSymbol Id -> Maybe Id
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup LocSymbol
x HashMap LocSymbol Id
defs
    let info = HasDebugCallStack => Id -> IdInfo
Id -> IdInfo
Ghc.idInfo Id
var
    let unfolding = Unfolding -> Maybe CoreExpr
getExprFromUnfolding (Unfolding -> Maybe CoreExpr)
-> (IdInfo -> Unfolding) -> IdInfo -> Maybe CoreExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IdInfo -> Unfolding
Ghc.realUnfoldingInfo (IdInfo -> Maybe CoreExpr) -> IdInfo -> Maybe CoreExpr
forall a b. (a -> b) -> a -> b
$ IdInfo
info
    case unfolding of
      Just CoreExpr
e ->
        (LocSymbol, Maybe SpecType, Id, CoreExpr)
-> Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr)
forall a. a -> Maybe a
Just (LocSymbol
x, LocSpecType -> SpecType
forall a. Located a -> a
val (LocSpecType -> SpecType) -> Maybe LocSpecType -> Maybe SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Id -> [(Id, LocSpecType)] -> Maybe LocSpecType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Id
var [(Id, LocSpecType)]
sigs, Id
var, CoreExpr
e)
      Maybe CoreExpr
_ ->
        Error -> Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr)
forall a e. (?callStack::CallStack, Exception e) => e -> a
Ex.throw (Error -> Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr))
-> Error -> Maybe (LocSymbol, Maybe SpecType, Id, CoreExpr)
forall a b. (a -> b) -> a -> b
$ LocSymbol -> [Char] -> Error
forall a. PPrint a => Located a -> [Char] -> Error
mkError LocSymbol
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 CoreExpr
getExprFromUnfolding (Ghc.CoreUnfolding CoreExpr
expr UnfoldingSource
_ Bool
_ UnfoldingCache
_ UnfoldingGuidance
_) = CoreExpr -> Maybe CoreExpr
forall a. a -> Maybe a
Just CoreExpr
expr
getExprFromUnfolding Unfolding
_ = Maybe CoreExpr
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
-> (LocSymbol, Maybe SpecType, Id, CoreExpr)
-> (Id, LocSpecType, Equation)
makeAxiom Env
env TycEnv
tycEnv LogicMap
lmap (LocSymbol
x, Maybe SpecType
mbT, Id
v, CoreExpr
def)
            = (Id
v, LocSpecType
t, Equation
e)
  where
    (LocSpecType
t, Equation
e)  = Config
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> LocSymbol
-> Maybe SpecType
-> Id
-> CoreExpr
-> (LocSpecType, Equation)
makeAssumeType (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env) TCEmb TyCon
embs LogicMap
lmap DataConMap
dm LocSymbol
x Maybe SpecType
mbT Id
v CoreExpr
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
-> LocSymbol
-> Maybe SpecType
-> Id
-> CoreExpr
-> (LocSpecType, Equation)
makeAssumeType Config
cfg TCEmb TyCon
tce LogicMap
lmap DataConMap
dm LocSymbol
sym Maybe SpecType
mbT Id
v CoreExpr
def
  = ( LocSymbol
sym {val = aty at `strengthenRes` F.subst su ref}
    , Symbol -> [(Symbol, Sort)] -> Expr -> 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 -> Expr -> Expr
F.sortSubstInExpr SortSubst
sortSub (Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
F.subst Subst
su Expr
le))
        (SortSubst -> Sort -> Sort
F.sortSubst SortSubst
sortSub Sort
out)
    )
  where
    allowTC :: Bool
allowTC = Config -> Bool
typeclass Config
cfg
    symbolV :: Symbol
symbolV = Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
v
    rt :: SpecType
rt    = RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
fromRTypeRep (RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType)
-> (SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft)
-> SpecType
-> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            (\trep :: RTypeRepV Symbol RTyCon RTyVar RReft
trep@RTypeRep{[(RTVar RTyVar (RRType ()), RReft)]
[Symbol]
[RReft]
[SpecType]
[PVarV Symbol (RRType ())]
[RFInfo]
SpecType
ty_res :: forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_args :: forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_refts :: forall v c tv r. RTypeRepV v c tv r -> [r]
ty_info :: forall v c tv r. RTypeRepV v c tv r -> [RFInfo]
ty_binds :: forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_preds :: forall v c tv r. RTypeRepV v c tv r -> [PVarV v (RTypeV v c tv ())]
ty_vars :: forall v c tv r.
RTypeRepV v c tv r -> [(RTVar tv (RTypeV v c tv ()), r)]
ty_vars :: [(RTVar RTyVar (RRType ()), RReft)]
ty_preds :: [PVarV Symbol (RRType ())]
ty_binds :: [Symbol]
ty_info :: [RFInfo]
ty_refts :: [RReft]
ty_args :: [SpecType]
ty_res :: SpecType
..} ->
                RTypeRepV Symbol RTyCon RTyVar RReft
trep{ty_info = fmap (\RFInfo
i -> RFInfo
i{permitTC = Just allowTC}) ty_info}) (RTypeRepV Symbol RTyCon RTyVar RReft
 -> RTypeRepV Symbol RTyCon RTyVar RReft)
-> (SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft)
-> SpecType
-> RTypeRepV Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ SpecType -> Maybe SpecType -> SpecType
forall a. a -> Maybe a -> a
Mb.fromMaybe (Kind -> SpecType
forall r. Monoid r => Kind -> RRType r
ofType Kind
τ) Maybe SpecType
mbT
    τ :: Kind
τ     = Id -> Kind
Ghc.varType Id
v
    at :: AxiomType
at    = Bool -> Symbol -> SpecType -> AxiomType
addSingletonApp Bool
allowTC Symbol
symbolV SpecType
rt
    out :: Sort
out   = TCEmb TyCon -> SpecType -> Sort
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RRType ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce (SpecType -> Sort) -> SpecType -> Sort
forall a b. (a -> b) -> a -> b
$ AxiomType -> SpecType
ares AxiomType
at
    xArgs :: [Expr]
xArgs = Symbol -> Expr
forall v. v -> ExprV v
F.EVar (Symbol -> Expr)
-> ((Symbol, SpecType) -> Symbol) -> (Symbol, SpecType) -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SpecType) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, SpecType) -> Expr) -> [(Symbol, SpecType)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AxiomType -> [(Symbol, SpecType)]
aargs AxiomType
at
    _msg :: [Char]
_msg  = [[Char]] -> [Char]
unwords [LocSymbol -> [Char]
forall a. PPrint a => a -> [Char]
showpp LocSymbol
sym, Maybe SpecType -> [Char]
forall a. PPrint a => a -> [Char]
showpp Maybe SpecType
mbT]
    le :: Expr
le    = case [Id]
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> Config
-> ([Char] -> Error)
-> LogicM Expr
-> Either Error Expr
forall t.
[Id]
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> Config
-> ([Char] -> Error)
-> LogicM t
-> Either Error t
runToLogicWithBoolBinds [Id]
bbs TCEmb TyCon
tce LogicMap
lmap DataConMap
dm Config
cfg [Char] -> Error
forall {t}. [Char] -> TError t
mkErr (CoreExpr -> LogicM Expr
coreToLogic CoreExpr
def') of
              Right Expr
e -> Expr
e
              Left  Error
e -> Error -> Expr
forall a e. (?callStack::CallStack, Exception e) => e -> a
Ex.throw Error
e
    ref :: Reft
ref        = (Symbol, Expr) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (Symbol
F.vv_, Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
F.PAtom Brel
F.Eq (Symbol -> Expr
forall v. v -> ExprV v
F.EVar Symbol
F.vv_) Expr
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
$ LocSymbol -> SourcePos
forall a. Located a -> SourcePos
loc LocSymbol
sym) (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (Symbol -> Doc) -> Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
sym) ([Char] -> Doc
PJ.text [Char]
s)
    bbs :: [Id]
bbs        = InterestingVarFun -> [Id] -> [Id]
forall a. (a -> Bool) -> [a] -> [a]
filter InterestingVarFun
isBoolBind [Id]
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) }
    ([Id]
tyVars, Kind
_) = Kind -> ([Id], Kind)
Ghc.splitForAllTyCoVars Kind
τ
    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 ((Id -> Symbol) -> [Id] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol [Id]
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 ..]

    ([Id]
xs, CoreExpr
def') = [Char] -> ([Id], CoreExpr) -> ([Id], CoreExpr)
forall a. Outputable a => [Char] -> a -> a
GM.notracePpr [Char]
"grabBody" (([Id], CoreExpr) -> ([Id], CoreExpr))
-> ([Id], CoreExpr) -> ([Id], CoreExpr)
forall a b. (a -> b) -> a -> b
$ Bool -> Kind -> CoreExpr -> ([Id], CoreExpr)
grabBody Bool
allowTC (Kind -> Kind
Ghc.expandTypeSynonyms Kind
τ) (CoreExpr -> ([Id], CoreExpr)) -> CoreExpr -> ([Id], CoreExpr)
forall a b. (a -> b) -> a -> b
$ Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
normalize Bool
allowTC CoreExpr
def
    su :: Subst
su         = [(Symbol, Expr)] -> Subst
F.mkSubst  ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol     (Id -> Symbol) -> [Id] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Id]
xs) [Expr]
xArgs
                           [(Symbol, Expr)] -> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. [a] -> [a] -> [a]
++ [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Id -> Symbol
forall t. NamedThing t => t -> Symbol
simplesymbol (Id -> Symbol) -> [Id] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Id]
xs) [Expr]
xArgs
    xts :: [(Symbol, Sort)]
xts        = [(Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Symbol
x, TCEmb TyCon -> SpecType -> Sort
rTypeSortExp TCEmb TyCon
tce SpecType
t) | (Symbol
x, SpecType
t) <- AxiomType -> [(Symbol, SpecType)]
aargs AxiomType
at]

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

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

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


isBoolBind :: Ghc.Var -> Bool
isBoolBind :: InterestingVarFun
isBoolBind Id
v = RRType () -> Bool
forall t t1. RType RTyCon t t1 -> Bool
isBool (RTypeRepV Symbol RTyCon RTyVar () -> RRType ()
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_res (RTypeRepV Symbol RTyCon RTyVar () -> RRType ())
-> RTypeRepV Symbol RTyCon RTyVar () -> RRType ()
forall a b. (a -> b) -> a -> b
$ RRType () -> RTypeRepV Symbol RTyCon RTyVar ()
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep ((Kind -> RRType ()
forall r. Monoid r => Kind -> RRType r
ofType (Kind -> RRType ()) -> Kind -> RRType ()
forall a b. (a -> b) -> a -> b
$ Id -> Kind
Ghc.varType Id
v) :: RRType ()))

strengthenRes :: SpecType -> F.Reft -> SpecType
strengthenRes :: SpecType -> Reft -> SpecType
strengthenRes SpecType
st Reft
rf = SpecType -> SpecType
forall {r} {v} {c} {tv}.
Reftable r =>
RTypeV v c tv r -> RTypeV v c tv r
go SpecType
st
  where
    go :: RTypeV v c tv r -> RTypeV v c tv r
go (RAllT RTVUV v c tv
a RTypeV v c tv r
t r
r)   = RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV v c tv
a (RTypeV v c tv r -> RTypeV v c tv r
go RTypeV v c tv r
t) r
r
    go (RAllP PVUV v c tv
p RTypeV v c tv r
t)     = PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV v c tv
p (RTypeV v c tv r -> RTypeV v c tv r)
-> RTypeV v c tv r -> RTypeV v c tv r
forall a b. (a -> b) -> a -> b
$ RTypeV v c tv r -> RTypeV v c tv r
go RTypeV v c tv r
t
    go (RFun Symbol
x RFInfo
i RTypeV v c tv r
tx RTypeV v c tv r
t r
r) = Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
x RFInfo
i RTypeV v c tv r
tx (RTypeV v c tv r -> RTypeV v c tv r
go RTypeV v c tv r
t) r
r
    go RTypeV v c tv r
t               =  RTypeV v c tv r
t RTypeV v c tv r -> r -> RTypeV v c tv r
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v c tv r
`strengthen` Reft -> r
forall r. Reftable r => Reft -> r
ofReft Reft
rf

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

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

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

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

data AxiomType = AT { AxiomType -> SpecType
aty :: SpecType, AxiomType -> [(Symbol, SpecType)]
aargs :: [(F.Symbol, SpecType)], AxiomType -> SpecType
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 -> SpecType -> AxiomType
addSingletonApp Bool
allowTC Symbol
s SpecType
st = SpecType -> [(Symbol, SpecType)] -> SpecType -> AxiomType
AT SpecType
to ([(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. [a] -> [a]
reverse [(Symbol, SpecType)]
xts) SpecType
res
  where
    (SpecType
to, (Int
_,[(Symbol, SpecType)]
xts, Just SpecType
res)) = State (Int, [(Symbol, SpecType)], Maybe SpecType) SpecType
-> (Int, [(Symbol, SpecType)], Maybe SpecType)
-> (SpecType, (Int, [(Symbol, SpecType)], Maybe SpecType))
forall s a. State s a -> s -> (a, s)
runState (SpecType
-> State (Int, [(Symbol, SpecType)], Maybe SpecType) SpecType
forall {m :: * -> *} {v} {t}.
Monad m =>
RTypeV v RTyCon t RReft
-> StateT
     (Int, [(Symbol, RTypeV v RTyCon t RReft)],
      Maybe (RTypeV v RTyCon t RReft))
     m
     (RTypeV v RTyCon t RReft)
go SpecType
st) (Int
1,[], Maybe SpecType
forall a. Maybe a
Nothing)
    go :: RTypeV v RTyCon t RReft
-> StateT
     (Int, [(Symbol, RTypeV v RTyCon t RReft)],
      Maybe (RTypeV v RTyCon t RReft))
     m
     (RTypeV v RTyCon t RReft)
go (RAllT RTVUV v RTyCon t
a RTypeV v RTyCon t RReft
t RReft
r) = RTVUV v RTyCon t
-> RTypeV v RTyCon t RReft -> RReft -> RTypeV v RTyCon t RReft
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV v RTyCon t
a (RTypeV v RTyCon t RReft -> RReft -> RTypeV v RTyCon t RReft)
-> StateT
     (Int, [(Symbol, RTypeV v RTyCon t RReft)],
      Maybe (RTypeV v RTyCon t RReft))
     m
     (RTypeV v RTyCon t RReft)
-> StateT
     (Int, [(Symbol, RTypeV v RTyCon t RReft)],
      Maybe (RTypeV v RTyCon t RReft))
     m
     (RReft -> RTypeV v RTyCon t RReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeV v RTyCon t RReft
-> StateT
     (Int, [(Symbol, RTypeV v RTyCon t RReft)],
      Maybe (RTypeV v RTyCon t RReft))
     m
     (RTypeV v RTyCon t RReft)
go RTypeV v RTyCon t RReft
t StateT
  (Int, [(Symbol, RTypeV v RTyCon t RReft)],
   Maybe (RTypeV v RTyCon t RReft))
  m
  (RReft -> RTypeV v RTyCon t RReft)
-> StateT
     (Int, [(Symbol, RTypeV v RTyCon t RReft)],
      Maybe (RTypeV v RTyCon t RReft))
     m
     RReft
-> StateT
     (Int, [(Symbol, RTypeV v RTyCon t RReft)],
      Maybe (RTypeV v RTyCon t RReft))
     m
     (RTypeV v RTyCon t RReft)
forall a b.
StateT
  (Int, [(Symbol, RTypeV v RTyCon t RReft)],
   Maybe (RTypeV v RTyCon t RReft))
  m
  (a -> b)
-> StateT
     (Int, [(Symbol, RTypeV v RTyCon t RReft)],
      Maybe (RTypeV v RTyCon t RReft))
     m
     a
-> StateT
     (Int, [(Symbol, RTypeV v RTyCon t RReft)],
      Maybe (RTypeV v RTyCon t RReft))
     m
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RReft
-> StateT
     (Int, [(Symbol, RTypeV v RTyCon t RReft)],
      Maybe (RTypeV v RTyCon t RReft))
     m
     RReft
forall a.
a
-> StateT
     (Int, [(Symbol, RTypeV v RTyCon t RReft)],
      Maybe (RTypeV v RTyCon t RReft))
     m
     a
forall (m :: * -> *) a. Monad m => a -> m a
return RReft
r
    go (RAllP PVUV v RTyCon t
p RTypeV v RTyCon t RReft
t) = PVUV v RTyCon t
-> RTypeV v RTyCon t RReft -> RTypeV v RTyCon t RReft
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV v RTyCon t
p (RTypeV v RTyCon t RReft -> RTypeV v RTyCon t RReft)
-> StateT
     (Int, [(Symbol, RTypeV v RTyCon t RReft)],
      Maybe (RTypeV v RTyCon t RReft))
     m
     (RTypeV v RTyCon t RReft)
-> StateT
     (Int, [(Symbol, RTypeV v RTyCon t RReft)],
      Maybe (RTypeV v RTyCon t RReft))
     m
     (RTypeV v RTyCon t RReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeV v RTyCon t RReft
-> StateT
     (Int, [(Symbol, RTypeV v RTyCon t RReft)],
      Maybe (RTypeV v RTyCon t RReft))
     m
     (RTypeV v RTyCon t RReft)
go RTypeV v RTyCon t RReft
t
    go (RFun Symbol
x RFInfo
i RTypeV v RTyCon t RReft
tx RTypeV v RTyCon t RReft
t RReft
r) | RTypeV v RTyCon t RReft -> Bool
forall {v} {t} {t1}. RTypeV v RTyCon t t1 -> Bool
isErasable RTypeV v RTyCon t RReft
tx = (\RTypeV v RTyCon t RReft
t' -> Symbol
-> RFInfo
-> RTypeV v RTyCon t RReft
-> RTypeV v RTyCon t RReft
-> RReft
-> RTypeV v RTyCon t RReft
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
x RFInfo
i RTypeV v RTyCon t RReft
tx RTypeV v RTyCon t RReft
t' RReft
r) (RTypeV v RTyCon t RReft -> RTypeV v RTyCon t RReft)
-> StateT
     (Int, [(Symbol, RTypeV v RTyCon t RReft)],
      Maybe (RTypeV v RTyCon t RReft))
     m
     (RTypeV v RTyCon t RReft)
-> StateT
     (Int, [(Symbol, RTypeV v RTyCon t RReft)],
      Maybe (RTypeV v RTyCon t RReft))
     m
     (RTypeV v RTyCon t RReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeV v RTyCon t RReft
-> StateT
     (Int, [(Symbol, RTypeV v RTyCon t RReft)],
      Maybe (RTypeV v RTyCon t RReft))
     m
     (RTypeV v RTyCon t RReft)
go RTypeV v RTyCon t RReft
t
    go (RFun Symbol
x RFInfo
ii RTypeV v RTyCon t RReft
tx RTypeV v RTyCon t RReft
t RReft
r) = do
      (i,bs,mres) <- StateT
  (Int, [(Symbol, RTypeV v RTyCon t RReft)],
   Maybe (RTypeV v RTyCon t RReft))
  m
  (Int, [(Symbol, RTypeV v RTyCon t RReft)],
   Maybe (RTypeV 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 RTypeV v RTyCon t RReft
t = do
      (i,bs,_) <- StateT
  (Int, [(Symbol, RTypeV v RTyCon t RReft)],
   Maybe (RTypeV v RTyCon t RReft))
  m
  (Int, [(Symbol, RTypeV v RTyCon t RReft)],
   Maybe (RTypeV 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, RTypeV v RTyCon t RReft) -> Symbol)
-> [(Symbol, RTypeV v RTyCon t RReft)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, RTypeV v RTyCon t RReft) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, RTypeV v RTyCon t RReft)]
bs
      let t' = RTypeV v RTyCon t RReft -> RReft -> RTypeV v RTyCon t RReft
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v c tv r
strengthen RTypeV 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 = Reft -> PredicateV Symbol -> RReft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft Reft
r PredicateV Symbol
forall a. Monoid a => a
mempty
  where
    r :: Reft
r             = Expr -> Reft
forall a. Expression a => a -> Reft
F.exprReft (Expr -> [Expr] -> Expr
forall v. ExprV v -> [ExprV v] -> ExprV v
F.eApps (Symbol -> Expr
forall v. v -> ExprV v
F.EVar Symbol
s) (a -> Expr
forall a. Symbolic a => a -> Expr
F.eVar (a -> Expr) -> [a] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
ys))