{-# LANGUAGE FlexibleContexts          #-}

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

module Language.Haskell.Liquid.Constraint.ToFixpoint
  ( cgInfoFInfo
  , fixConfig
  , refinementEQs
  , canRewrite
  ) where

import           Prelude hiding (error)
import qualified Liquid.GHC.API as Ghc
import           Liquid.GHC.API (Var, Id, TyCon)
import qualified Language.Fixpoint.Types.Config as FC
import           System.Console.CmdArgs.Default (def)
import qualified Language.Fixpoint.Types        as F
import           Language.Fixpoint.Solver.Rewrite (unify)
import           Language.Haskell.Liquid.Constraint.Types
import qualified Language.Haskell.Liquid.Types.RefType as RT
import           Language.Haskell.Liquid.Constraint.Qualifier
import           Control.Monad (guard)
import qualified Data.Maybe as Mb

-- AT: Move to own module?
-- imports for AxiomEnv
import           Language.Haskell.Liquid.UX.Config
import           Language.Haskell.Liquid.UX.DiffCheck (coreDefs, coreDeps, dependsOn, Def(..))
import qualified Language.Haskell.Liquid.GHC.Misc  as GM -- (simplesymbol)
import qualified Data.List                         as L
import qualified Data.HashMap.Strict               as M
import qualified Data.HashSet                      as S
-- import           Language.Fixpoint.Misc
import qualified Language.Haskell.Liquid.Misc      as Misc

import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.Types hiding     ( binds )

fixConfig :: FilePath -> Config -> FC.Config
fixConfig :: FilePath -> Config -> Config
fixConfig FilePath
tgt Config
cfg = Config
forall a. Default a => a
def
  { FC.solver                   = Mb.fromJust (smtsolver cfg)
  , FC.linear                   = linear            cfg
  , FC.eliminate                = eliminate         cfg
  , FC.nonLinCuts               = not (higherOrderFlag cfg) -- eliminate cfg /= FC.All
  , FC.save                     = saveQuery         cfg
  , FC.srcFile                  = tgt
  , FC.cores                    = cores             cfg
  , FC.minPartSize              = minPartSize       cfg
  , FC.maxPartSize              = maxPartSize       cfg
  , FC.elimStats                = elimStats         cfg
  , FC.elimBound                = elimBound         cfg
  , FC.allowHO                  = higherOrderFlag   cfg
  , FC.allowHOqs                = higherorderqs     cfg
  , FC.smtTimeout               = smtTimeout        cfg
  , FC.stringTheory             = stringTheory      cfg
  , FC.gradual                  = gradual           cfg
  , FC.ginteractive             = ginteractive       cfg
  , FC.noslice                  = noslice           cfg
  , FC.rewriteAxioms            = allowPLE   cfg
  , FC.pleWithUndecidedGuards   = pleWithUndecidedGuards cfg
  , FC.etabeta                  = etabeta    cfg
  , FC.localRewrites            = dependantCase cfg
  , FC.etaElim                  = not (exactDC cfg) && extensionality cfg -- SEE: https://github.com/ucsd-progsys/liquidhaskell/issues/1601
  , FC.extensionality           = extensionality    cfg
  , FC.interpreter              = interpreter    cfg
  , FC.oldPLE                   = oldPLE cfg
  , FC.rwTerminationCheck       = rwTerminationCheck cfg
  , FC.noLazyPLE                = noLazyPLE cfg
  , FC.fuel                     = fuel      cfg
  , FC.noEnvironmentReduction   = not (environmentReduction cfg)
  , FC.inlineANFBindings        = inlineANFBindings cfg
  }

cgInfoFInfo :: TargetInfo -> CGInfo -> IO (F.FInfo Cinfo)
cgInfoFInfo :: TargetInfo -> CGInfo -> IO (FInfo Cinfo)
cgInfoFInfo TargetInfo
info CGInfo
cgi = FInfo Cinfo -> IO (FInfo Cinfo)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (TargetInfo -> CGInfo -> FInfo Cinfo
targetFInfo TargetInfo
info CGInfo
cgi)

targetFInfo :: TargetInfo -> CGInfo -> F.FInfo Cinfo
targetFInfo :: TargetInfo -> CGInfo -> FInfo Cinfo
targetFInfo TargetInfo
info CGInfo
cgi = FInfo Cinfo -> FInfo Cinfo -> FInfo Cinfo
forall a. Monoid a => a -> a -> a
mappend (FInfo Cinfo
forall a. Monoid a => a
mempty { F.ae = ax, F.lrws = localRewrites cgi }) FInfo Cinfo
fi
  where
    fi :: FInfo Cinfo
fi               = [SubC Cinfo]
-> [WfC Cinfo]
-> BindEnv Cinfo
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap Int Cinfo
-> Bool
-> Bool
-> [Triggered (ExprV Symbol)]
-> AxiomEnv
-> [DataDecl]
-> [Int]
-> FInfo Cinfo
forall a.
[SubC a]
-> [WfC a]
-> BindEnv a
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap Int a
-> Bool
-> Bool
-> [Triggered (ExprV Symbol)]
-> AxiomEnv
-> [DataDecl]
-> [Int]
-> GInfo SubC a
F.fi [SubC Cinfo]
cs [WfC Cinfo]
ws BindEnv Cinfo
bs SEnv Sort
ls SEnv Sort
consts Kuts
ks [Qualifier]
qs HashMap Int Cinfo
bi Bool
aHO Bool
aHOqs [Triggered (ExprV Symbol)]
forall {a}. [a]
es AxiomEnv
forall a. Monoid a => a
mempty [DataDecl]
adts [Int]
ebs
    cs :: [SubC Cinfo]
cs               = CGInfo -> [SubC Cinfo]
fixCs    CGInfo
cgi
    ws :: [WfC Cinfo]
ws               = CGInfo -> [WfC Cinfo]
fixWfs   CGInfo
cgi
    bs :: BindEnv Cinfo
bs               = CGInfo -> BindEnv Cinfo
binds    CGInfo
cgi
    ebs :: [Int]
ebs              = CGInfo -> [Int]
ebinds   CGInfo
cgi
    ls :: SEnv Sort
ls               = CGInfo -> SEnv Sort
fEnv     CGInfo
cgi
    consts :: SEnv Sort
consts           = CGInfo -> SEnv Sort
cgConsts CGInfo
cgi
    ks :: Kuts
ks               = CGInfo -> Kuts
kuts     CGInfo
cgi
    adts :: [DataDecl]
adts             = CGInfo -> [DataDecl]
cgADTs   CGInfo
cgi
    qs :: [Qualifier]
qs               = TargetInfo -> SEnv Sort -> [Qualifier]
giQuals TargetInfo
info (CGInfo -> SEnv Sort
fEnv CGInfo
cgi)
    bi :: HashMap Int Cinfo
bi               = (\SrcSpan
x -> SrcSpan -> Maybe Error -> Maybe Var -> Cinfo
Ci SrcSpan
x Maybe Error
forall a. Maybe a
Nothing Maybe Var
forall a. Maybe a
Nothing) (SrcSpan -> Cinfo) -> HashMap Int SrcSpan -> HashMap Int Cinfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGInfo -> HashMap Int SrcSpan
bindSpans CGInfo
cgi
    aHO :: Bool
aHO              = CGInfo -> Bool
allowHO CGInfo
cgi
    aHOqs :: Bool
aHOqs            = TargetInfo -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag TargetInfo
info
    es :: [a]
es               = [] -- makeAxioms info
    ax :: AxiomEnv
ax               = TargetInfo
-> [(Var, SpecType)] -> HashMap SubcId (SubC Cinfo) -> AxiomEnv
makeAxiomEnvironment TargetInfo
info (CGInfo -> [(Var, SpecType)]
dataConTys CGInfo
cgi) (FInfo Cinfo -> HashMap SubcId (SubC Cinfo)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm FInfo Cinfo
fi)
    -- msg              = show . map F.symbol . M.keys . tyConInfo

makeAxiomEnvironment :: TargetInfo -> [(Var, SpecType)] -> M.HashMap F.SubcId (F.SubC Cinfo) -> F.AxiomEnv
makeAxiomEnvironment :: TargetInfo
-> [(Var, SpecType)] -> HashMap SubcId (SubC Cinfo) -> AxiomEnv
makeAxiomEnvironment TargetInfo
info [(Var, SpecType)]
xts HashMap SubcId (SubC Cinfo)
fcs
  = [Equation]
-> [Rewrite]
-> HashMap SubcId Bool
-> HashMap SubcId [AutoRewrite]
-> AxiomEnv
F.AEnv [Equation]
eqs
           (((Var, SpecType) -> [Rewrite]) -> [(Var, SpecType)] -> [Rewrite]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Var, SpecType) -> [Rewrite]
makeSimplify [(Var, SpecType)]
xts)
           (TargetSpec -> Config -> SubC Cinfo -> Bool
doExpand TargetSpec
sp Config
cfg (SubC Cinfo -> Bool)
-> HashMap SubcId (SubC Cinfo) -> HashMap SubcId Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap SubcId (SubC Cinfo)
fcs)
           (TargetInfo -> SubC Cinfo -> [AutoRewrite]
makeRewrites TargetInfo
info (SubC Cinfo -> [AutoRewrite])
-> HashMap SubcId (SubC Cinfo) -> HashMap SubcId [AutoRewrite]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap SubcId (SubC Cinfo)
fcs)
  where
    eqs :: [Equation]
eqs      = if Config -> Bool
oldPLE Config
cfg
                then Bool -> TargetSpec -> [Equation]
makeEquations (Config -> Bool
typeclass Config
cfg) TargetSpec
sp [Equation] -> [Equation] -> [Equation]
forall a. [a] -> [a] -> [a]
++ ((Var, SpecType) -> Equation) -> [(Var, SpecType)] -> [Equation]
forall a b. (a -> b) -> [a] -> [b]
map ((Var -> SpecType -> Equation) -> (Var, SpecType) -> Equation
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Var -> SpecType -> Equation) -> (Var, SpecType) -> Equation)
-> (Var -> SpecType -> Equation) -> (Var, SpecType) -> Equation
forall a b. (a -> b) -> a -> b
$ TCEmb TyCon -> Var -> SpecType -> Equation
specTypeEq TCEmb TyCon
emb) [(Var, SpecType)]
xts
                else [Equation]
axioms
    emb :: TCEmb TyCon
emb      = GhcSpecNames -> TCEmb TyCon
gsTcEmbeds (TargetSpec -> GhcSpecNames
gsName TargetSpec
sp)
    cfg :: Config
cfg      = TargetInfo -> Config
forall t. HasConfig t => t -> Config
getConfig  TargetInfo
info
    sp :: TargetSpec
sp       = TargetInfo -> TargetSpec
giSpec     TargetInfo
info
    axioms :: [Equation]
axioms   = GhcSpecRefl -> [Equation]
gsMyAxioms GhcSpecRefl
refl [Equation] -> [Equation] -> [Equation]
forall a. [a] -> [a] -> [a]
++ GhcSpecRefl -> [Equation]
gsImpAxioms GhcSpecRefl
refl
    refl :: GhcSpecRefl
refl     = TargetSpec -> GhcSpecRefl
gsRefl TargetSpec
sp


makeRewrites :: TargetInfo -> F.SubC Cinfo -> [F.AutoRewrite]
makeRewrites :: TargetInfo -> SubC Cinfo -> [AutoRewrite]
makeRewrites TargetInfo
info SubC Cinfo
sub = ((Var, LocSpecType) -> [AutoRewrite])
-> [(Var, LocSpecType)] -> [AutoRewrite]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (TCEmb TyCon -> (Var, LocSpecType) -> [AutoRewrite]
makeRewriteOne TCEmb TyCon
tce) ([(Var, LocSpecType)] -> [AutoRewrite])
-> [(Var, LocSpecType)] -> [AutoRewrite]
forall a b. (a -> b) -> a -> b
$ ((Var, LocSpecType) -> Bool)
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Var -> HashSet Var -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Var
rws) (Var -> Bool)
-> ((Var, LocSpecType) -> Var) -> (Var, LocSpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, LocSpecType) -> Var
forall a b. (a, b) -> a
fst) [(Var, LocSpecType)]
sigs
  where
    tce :: TCEmb TyCon
tce        = GhcSpecNames -> TCEmb TyCon
gsTcEmbeds (TargetSpec -> GhcSpecNames
gsName TargetSpec
spec)
    spec :: TargetSpec
spec       = TargetInfo -> TargetSpec
giSpec TargetInfo
info
    sig :: GhcSpecSig
sig        = TargetSpec -> GhcSpecSig
gsSig TargetSpec
spec
    sigs :: [(Var, LocSpecType)]
sigs       = GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs GhcSpecSig
sig [(Var, LocSpecType)]
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs GhcSpecSig
sig
    isGlobalRw :: Bool
isGlobalRw = Bool -> (Var -> Bool) -> Maybe Var -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe Bool
False (Var -> HashSet Var -> Bool
forall a. Eq a => a -> HashSet a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` HashSet Var
globalRws) Maybe Var
parentFunction

    parentFunction :: Maybe Var
    parentFunction :: Maybe Var
parentFunction =
      case SubC Cinfo -> Maybe Var
subVar SubC Cinfo
sub of
        Just Var
v -> Var -> Maybe Var
forall a. a -> Maybe a
Just Var
v
        Maybe Var
Nothing ->
          [Var] -> Maybe Var
forall a. [a] -> Maybe a
Mb.listToMaybe ([Var] -> Maybe Var) -> [Var] -> Maybe Var
forall a b. (a -> b) -> a -> b
$ do
            D s e v <- [CoreBind] -> [Def]
coreDefs ([CoreBind] -> [Def]) -> [CoreBind] -> [Def]
forall a b. (a -> b) -> a -> b
$ TargetSrc -> [CoreBind]
giCbs (TargetSrc -> [CoreBind]) -> TargetSrc -> [CoreBind]
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSrc
giSrc TargetInfo
info
            let (Ghc.RealSrcSpan cc _) = ci_loc $ F.sinfo sub
            guard $ s <= Ghc.srcSpanStartLine cc && e >= Ghc.srcSpanEndLine cc
            return v

    rws :: HashSet Var
rws =
      if Bool
isGlobalRw
      then HashSet Var
forall a. HashSet a
S.empty
      else HashSet Var -> HashSet Var -> HashSet Var
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference
        (HashSet Var -> HashSet Var -> HashSet Var
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union HashSet Var
localRws HashSet Var
globalRws)
        (HashSet Var -> (Var -> HashSet Var) -> Maybe Var -> HashSet Var
forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe HashSet Var
forall a. HashSet a
S.empty Var -> HashSet Var
forbiddenRWs Maybe Var
parentFunction)

    allDeps :: Deps
allDeps         = [CoreBind] -> Deps
coreDeps ([CoreBind] -> Deps) -> [CoreBind] -> Deps
forall a b. (a -> b) -> a -> b
$ TargetSrc -> [CoreBind]
giCbs (TargetSrc -> [CoreBind]) -> TargetSrc -> [CoreBind]
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSrc
giSrc TargetInfo
info
    forbiddenRWs :: Var -> HashSet Var
forbiddenRWs Var
sv =
      Var -> HashSet Var -> HashSet Var
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert Var
sv (HashSet Var -> HashSet Var) -> HashSet Var -> HashSet Var
forall a b. (a -> b) -> a -> b
$ Deps -> [Var] -> HashSet Var
dependsOn Deps
allDeps [Var
sv]

    localRws :: HashSet Var
localRws = HashSet Var -> Maybe (HashSet Var) -> HashSet Var
forall a. a -> Maybe a -> a
Mb.fromMaybe HashSet Var
forall a. HashSet a
S.empty (Maybe (HashSet Var) -> HashSet Var)
-> Maybe (HashSet Var) -> HashSet Var
forall a b. (a -> b) -> a -> b
$ do
      var    <- Maybe Var
parentFunction
      usable <- M.lookup var $ gsRewritesWith $ gsRefl spec
      return $ S.fromList usable

    globalRws :: HashSet Var
globalRws = (Located Var -> Var) -> HashSet (Located Var) -> HashSet Var
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map Located Var -> Var
forall a. Located a -> a
val (HashSet (Located Var) -> HashSet Var)
-> HashSet (Located Var) -> HashSet Var
forall a b. (a -> b) -> a -> b
$ GhcSpecRefl -> HashSet (Located Var)
gsRewrites (GhcSpecRefl -> HashSet (Located Var))
-> GhcSpecRefl -> HashSet (Located Var)
forall a b. (a -> b) -> a -> b
$ TargetSpec -> GhcSpecRefl
gsRefl TargetSpec
spec


canRewrite :: S.HashSet F.Symbol -> F.Expr -> F.Expr -> Bool
canRewrite :: HashSet Symbol -> ExprV Symbol -> ExprV Symbol -> Bool
canRewrite HashSet Symbol
freeVars' ExprV Symbol
from ExprV Symbol
to = Bool
noFreeSyms Bool -> Bool -> Bool
&& Bool
doesNotDiverge
  where
    fromSyms :: HashSet Symbol
fromSyms           = HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.intersection HashSet Symbol
freeVars' ([Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ ExprV Symbol -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms ExprV Symbol
from)
    toSyms :: HashSet Symbol
toSyms             = HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.intersection HashSet Symbol
freeVars' ([Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ ExprV Symbol -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms ExprV Symbol
to)
    noFreeSyms :: Bool
noFreeSyms         = HashSet Symbol -> Bool
forall a. HashSet a -> Bool
S.null (HashSet Symbol -> Bool) -> HashSet Symbol -> Bool
forall a b. (a -> b) -> a -> b
$ HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference HashSet Symbol
toSyms HashSet Symbol
fromSyms
    doesNotDiverge :: Bool
doesNotDiverge     = Maybe Subst -> Bool
forall a. Maybe a -> Bool
Mb.isNothing ([Symbol] -> ExprV Symbol -> ExprV Symbol -> Maybe Subst
unify (HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
S.toList HashSet Symbol
freeVars') ExprV Symbol
from ExprV Symbol
to)
                      Bool -> Bool -> Bool
|| Maybe Subst -> Bool
forall a. Maybe a -> Bool
Mb.isJust ([Symbol] -> ExprV Symbol -> ExprV Symbol -> Maybe Subst
unify (HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
S.toList HashSet Symbol
freeVars') ExprV Symbol
to ExprV Symbol
from)

refinementEQs :: LocSpecType -> [(F.Expr, F.Expr)]
refinementEQs :: LocSpecType -> [(ExprV Symbol, ExprV Symbol)]
refinementEQs LocSpecType
t =
  case SpecType -> Maybe RReft
forall c tv r. RType c tv r -> Maybe r
stripRTypeBase SpecType
tres of
    Just RReft
r ->
      [ (ExprV Symbol
lhs, ExprV Symbol
rhs) | (F.EEq ExprV Symbol
lhs ExprV Symbol
rhs) <- ExprV Symbol -> [ExprV Symbol]
F.splitPAnd (ExprV Symbol -> [ExprV Symbol]) -> ExprV Symbol -> [ExprV Symbol]
forall a b. (a -> b) -> a -> b
$ ReftV Symbol -> ExprV Symbol
forall v. ReftV v -> ExprV v
F.reftPred (RReft -> ReftV Symbol
forall r. Reftable r => r -> ReftV Symbol
toReft RReft
r) ]
    Maybe RReft
Nothing ->
      []
  where
    tres :: SpecType
tres = RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_res RTypeRepV Symbol RTyCon RTyVar RReft
tRep
    tRep :: RTypeRepV Symbol RTyCon RTyVar RReft
tRep = SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep (SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft)
-> SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
t

makeRewriteOne :: F.TCEmb TyCon -> (Var, LocSpecType) -> [F.AutoRewrite]
makeRewriteOne :: TCEmb TyCon -> (Var, LocSpecType) -> [AutoRewrite]
makeRewriteOne TCEmb TyCon
tce (Var
_, LocSpecType
t)
  = [AutoRewrite
rw | (ExprV Symbol
lhs, ExprV Symbol
rhs) <- LocSpecType -> [(ExprV Symbol, ExprV Symbol)]
refinementEQs LocSpecType
t , AutoRewrite
rw <- ExprV Symbol -> ExprV Symbol -> [AutoRewrite]
rewrites ExprV Symbol
lhs ExprV Symbol
rhs ]
  where

    rewrites :: F.Expr -> F.Expr -> [F.AutoRewrite]
    rewrites :: ExprV Symbol -> ExprV Symbol -> [AutoRewrite]
rewrites ExprV Symbol
lhs ExprV Symbol
rhs =
         (Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (HashSet Symbol -> ExprV Symbol -> ExprV Symbol -> Bool
canRewrite HashSet Symbol
freeVars' ExprV Symbol
lhs ExprV Symbol
rhs) [()] -> [AutoRewrite] -> [AutoRewrite]
forall a b. [a] -> [b] -> [b]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [[SortedReft] -> ExprV Symbol -> ExprV Symbol -> AutoRewrite
F.AutoRewrite [SortedReft]
xs ExprV Symbol
lhs ExprV Symbol
rhs])
      [AutoRewrite] -> [AutoRewrite] -> [AutoRewrite]
forall a. [a] -> [a] -> [a]
++ (Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (HashSet Symbol -> ExprV Symbol -> ExprV Symbol -> Bool
canRewrite HashSet Symbol
freeVars' ExprV Symbol
rhs ExprV Symbol
lhs) [()] -> [AutoRewrite] -> [AutoRewrite]
forall a b. [a] -> [b] -> [b]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [[SortedReft] -> ExprV Symbol -> ExprV Symbol -> AutoRewrite
F.AutoRewrite [SortedReft]
xs ExprV Symbol
rhs ExprV Symbol
lhs])

    freeVars' :: HashSet Symbol
freeVars' = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (RTypeRepV Symbol RTyCon RTyVar RReft -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV Symbol RTyCon RTyVar RReft
tRep)

    xs :: [SortedReft]
xs = do
      (sym, arg) <- [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRepV Symbol RTyCon RTyVar RReft -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV Symbol RTyCon RTyVar RReft
tRep) (RTypeRepV Symbol RTyCon RTyVar RReft -> [SpecType]
forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_args RTypeRepV Symbol RTyCon RTyVar RReft
tRep)
      let e = ExprV Symbol
-> (RReft -> ExprV Symbol) -> Maybe RReft -> ExprV Symbol
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ExprV Symbol
forall v. ExprV v
F.PTrue (ReftV Symbol -> ExprV Symbol
forall v. ReftV v -> ExprV v
F.reftPred (ReftV Symbol -> ExprV Symbol)
-> (RReft -> ReftV Symbol) -> RReft -> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RReft -> ReftV Symbol
forall r. Reftable r => r -> ReftV Symbol
toReft) (SpecType -> Maybe RReft
forall c tv r. RType c tv r -> Maybe r
stripRTypeBase SpecType
arg)
      return $ F.RR (RT.rTypeSort tce arg) (F.Reft (sym, e))

    tRep :: RTypeRepV Symbol RTyCon RTyVar RReft
tRep = SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep (SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft)
-> SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
t

_isClassOrDict :: Id -> Bool
_isClassOrDict :: Var -> Bool
_isClassOrDict Var
x = FilePath -> Bool -> Bool
forall a. PPrint a => FilePath -> a -> a
F.tracepp (FilePath
"isClassOrDict: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Var -> FilePath
forall a. PPrint a => a -> FilePath
F.showpp Var
x) (Var -> Bool
hasClassArg Var
x Bool -> Bool -> Bool
|| Var -> Bool
forall a. Symbolic a => a -> Bool
GM.isDictionary Var
x Bool -> Bool -> Bool
|| Maybe Class -> Bool
forall a. Maybe a -> Bool
Mb.isJust (Var -> Maybe Class
Ghc.isClassOpId_maybe Var
x))

hasClassArg :: Id -> Bool
hasClassArg :: Var -> Bool
hasClassArg Var
x = FilePath -> Bool -> Bool
forall a. PPrint a => FilePath -> a -> a
F.tracepp FilePath
msg (Var -> Bool
GM.isDataConId Var
x Bool -> Bool -> Bool
&& (PredType -> Bool) -> [PredType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any PredType -> Bool
Ghc.isClassPred (PredType
tPredType -> [PredType] -> [PredType]
forall a. a -> [a] -> [a]
:[PredType]
ts'))
  where
    msg :: FilePath
msg       = FilePath
"hasClassArg: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Var, [PredType]) -> FilePath
forall a. PPrint a => a -> FilePath
showpp (Var
x, PredType
tPredType -> [PredType] -> [PredType]
forall a. a -> [a] -> [a]
:[PredType]
ts')
    ([Scaled PredType]
ts, PredType
t)   = PredType -> ([Scaled PredType], PredType)
Ghc.splitFunTys (PredType -> ([Scaled PredType], PredType))
-> (Var -> PredType) -> Var -> ([Scaled PredType], PredType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Var], PredType) -> PredType
forall a b. (a, b) -> b
snd (([Var], PredType) -> PredType)
-> (Var -> ([Var], PredType)) -> Var -> PredType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> ([Var], PredType)
Ghc.splitForAllTyCoVars (PredType -> ([Var], PredType))
-> (Var -> PredType) -> Var -> ([Var], PredType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> PredType
Ghc.varType (Var -> ([Scaled PredType], PredType))
-> Var -> ([Scaled PredType], PredType)
forall a b. (a -> b) -> a -> b
$ Var
x
    ts' :: [PredType]
ts'       = (Scaled PredType -> PredType) -> [Scaled PredType] -> [PredType]
forall a b. (a -> b) -> [a] -> [b]
map Scaled PredType -> PredType
forall a. Scaled a -> a
Ghc.irrelevantMult [Scaled PredType]
ts


doExpand :: TargetSpec -> Config -> F.SubC Cinfo -> Bool
doExpand :: TargetSpec -> Config -> SubC Cinfo -> Bool
doExpand TargetSpec
sp Config
cfg SubC Cinfo
sub = Config -> Bool
allowGlobalPLE Config
cfg
                   Bool -> Bool -> Bool
|| (Config -> Bool
allowLocalPLE Config
cfg Bool -> Bool -> Bool
&& Bool -> (Var -> Bool) -> Maybe Var -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (TargetSpec -> Var -> Bool
isPLEVar TargetSpec
sp) (SubC Cinfo -> Maybe Var
subVar SubC Cinfo
sub))

-- [TODO:missing-sorts] data-constructors often have unelaboratable 'define' so either
-- 1. Make `elaborate` robust so it doesn't crash and returns maybe or
-- 2. Make the `ctor` well-sorted or 
-- 3. Don't create `define` for the ctor. 
-- Unfortunately 3 breaks a bunch of tests...

specTypeEq :: F.TCEmb TyCon -> Var -> SpecType -> F.Equation
specTypeEq :: TCEmb TyCon -> Var -> SpecType -> Equation
specTypeEq TCEmb TyCon
emb Var
f SpecType
t = Symbol -> [(Symbol, Sort)] -> ExprV Symbol -> Sort -> Equation
F.mkEquation (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
f) [(Symbol, Sort)]
xts ExprV Symbol
body Sort
tOut
  where
    xts :: [(Symbol, Sort)]
xts            = FilePath -> [Symbol] -> [Sort] -> [(Symbol, Sort)]
forall t t1. FilePath -> [t] -> [t1] -> [(t, t1)]
Misc.safeZipWithError FilePath
"specTypeEq" [Symbol]
xs (TCEmb TyCon -> SpecType -> Sort
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
RT.rTypeSort TCEmb TyCon
emb (SpecType -> Sort) -> [SpecType] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts)
    body :: ExprV Symbol
body           = ExprV Symbol -> SpecType -> ExprV Symbol
specTypeToResultRef ExprV Symbol
bExp SpecType
t
    tOut :: Sort
tOut           = TCEmb TyCon -> SpecType -> Sort
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
RT.rTypeSort TCEmb TyCon
emb (RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_res RTypeRepV Symbol RTyCon RTyVar RReft
tRep)
    tRep :: RTypeRepV Symbol RTyCon RTyVar RReft
tRep           = SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep SpecType
t
    xs :: [Symbol]
xs             = RTypeRepV Symbol RTyCon RTyVar RReft -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV Symbol RTyCon RTyVar RReft
tRep
    ts :: [SpecType]
ts             = RTypeRepV Symbol RTyCon RTyVar RReft -> [SpecType]
forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_args  RTypeRepV Symbol RTyCon RTyVar RReft
tRep
    bExp :: ExprV Symbol
bExp           = ExprV Symbol -> [ExprV Symbol] -> ExprV Symbol
forall v. ExprV v -> [ExprV v] -> ExprV v
F.eApps (Var -> ExprV Symbol
forall a. Symbolic a => a -> ExprV Symbol
F.eVar Var
f) (Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar (Symbol -> ExprV Symbol) -> [Symbol] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs)

makeSimplify :: (Var, SpecType) -> [F.Rewrite]
makeSimplify :: (Var, SpecType) -> [Rewrite]
makeSimplify (Var
var, SpecType
t)
  | Bool -> Bool
not (Var -> Bool
GM.isDataConId Var
var)
  = []
  | Bool
otherwise
  = ExprV Symbol -> [Rewrite]
go (ExprV Symbol -> [Rewrite]) -> ExprV Symbol -> [Rewrite]
forall a b. (a -> b) -> a -> b
$ ExprV Symbol -> SpecType -> ExprV Symbol
specTypeToResultRef (ExprV Symbol -> [ExprV Symbol] -> ExprV Symbol
forall v. ExprV v -> [ExprV v] -> ExprV v
F.eApps (Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar (Symbol -> ExprV Symbol) -> Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
var) (Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar (Symbol -> ExprV Symbol) -> [Symbol] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeRepV Symbol RTyCon RTyVar RReft -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds (SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep SpecType
t))) SpecType
t
  where
    go :: ExprV Symbol -> [Rewrite]
go (F.PAnd [ExprV Symbol]
es) = (ExprV Symbol -> [Rewrite]) -> [ExprV Symbol] -> [Rewrite]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ExprV Symbol -> [Rewrite]
go [ExprV Symbol]
es

    go (F.PAtom Brel
eq (F.EApp (F.EVar Symbol
f) ExprV Symbol
expr) ExprV Symbol
bd)
      | Brel
eq Brel -> [Brel] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Brel
F.Eq, Brel
F.Ueq]
      , (F.EVar Symbol
dc, [ExprV Symbol]
xs) <- ExprV Symbol -> (ExprV Symbol, [ExprV Symbol])
forall v. ExprV v -> (ExprV v, [ExprV v])
F.splitEApp ExprV Symbol
expr
      , Symbol
dc Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
var
      , (ExprV Symbol -> Bool) -> [ExprV Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ExprV Symbol -> Bool
forall {v}. ExprV v -> Bool
isEVar [ExprV Symbol]
xs
      = [Symbol -> Symbol -> [Symbol] -> ExprV Symbol -> Rewrite
F.SMeasure Symbol
f Symbol
dc (ExprV Symbol -> Symbol
forall {v}. ExprV v -> v
fromEVar (ExprV Symbol -> Symbol) -> [ExprV Symbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprV Symbol]
xs) ExprV Symbol
bd]

    go (F.PIff (F.EApp (F.EVar Symbol
f) ExprV Symbol
expr) ExprV Symbol
bd)
      | (F.EVar Symbol
dc, [ExprV Symbol]
xs) <- ExprV Symbol -> (ExprV Symbol, [ExprV Symbol])
forall v. ExprV v -> (ExprV v, [ExprV v])
F.splitEApp ExprV Symbol
expr
      , Symbol
dc Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
var
      , (ExprV Symbol -> Bool) -> [ExprV Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ExprV Symbol -> Bool
forall {v}. ExprV v -> Bool
isEVar [ExprV Symbol]
xs
      = [Symbol -> Symbol -> [Symbol] -> ExprV Symbol -> Rewrite
F.SMeasure Symbol
f Symbol
dc (ExprV Symbol -> Symbol
forall {v}. ExprV v -> v
fromEVar (ExprV Symbol -> Symbol) -> [ExprV Symbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprV Symbol]
xs) ExprV Symbol
bd]

    go (F.EApp (F.EVar Symbol
f) ExprV Symbol
expr)
      | (F.EVar Symbol
dc, [ExprV Symbol]
xs) <- ExprV Symbol -> (ExprV Symbol, [ExprV Symbol])
forall v. ExprV v -> (ExprV v, [ExprV v])
F.splitEApp ExprV Symbol
expr
      , Symbol
dc Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
var
      , (ExprV Symbol -> Bool) -> [ExprV Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ExprV Symbol -> Bool
forall {v}. ExprV v -> Bool
isEVar [ExprV Symbol]
xs
      = [Symbol -> Symbol -> [Symbol] -> ExprV Symbol -> Rewrite
F.SMeasure Symbol
f Symbol
dc (ExprV Symbol -> Symbol
forall {v}. ExprV v -> v
fromEVar (ExprV Symbol -> Symbol) -> [ExprV Symbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprV Symbol]
xs) ExprV Symbol
forall v. ExprV v
F.PTrue]

    go (F.PNot (F.EApp (F.EVar Symbol
f) ExprV Symbol
expr))
      | (F.EVar Symbol
dc, [ExprV Symbol]
xs) <- ExprV Symbol -> (ExprV Symbol, [ExprV Symbol])
forall v. ExprV v -> (ExprV v, [ExprV v])
F.splitEApp ExprV Symbol
expr
      , Symbol
dc Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
var
      , (ExprV Symbol -> Bool) -> [ExprV Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ExprV Symbol -> Bool
forall {v}. ExprV v -> Bool
isEVar [ExprV Symbol]
xs
      = [Symbol -> Symbol -> [Symbol] -> ExprV Symbol -> Rewrite
F.SMeasure Symbol
f Symbol
dc (ExprV Symbol -> Symbol
forall {v}. ExprV v -> v
fromEVar (ExprV Symbol -> Symbol) -> [ExprV Symbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprV Symbol]
xs) ExprV Symbol
forall v. ExprV v
F.PFalse]

    go ExprV Symbol
_ = []

    isEVar :: ExprV v -> Bool
isEVar (F.EVar v
_) = Bool
True
    isEVar ExprV v
_ = Bool
False

    fromEVar :: ExprV v -> v
fromEVar (F.EVar v
x) = v
x
    fromEVar ExprV v
_ = Maybe SrcSpan -> FilePath -> v
forall a. Maybe SrcSpan -> FilePath -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing FilePath
"makeSimplify.fromEVar"

makeEquations :: Bool -> TargetSpec -> [F.Equation]
makeEquations :: Bool -> TargetSpec -> [Equation]
makeEquations Bool
allowTC TargetSpec
sp = [ Symbol -> [(Symbol, Sort)] -> ExprV Symbol -> Sort -> Equation
F.mkEquation Symbol
f [(Symbol, Sort)]
xts (Bool
-> ExprV Symbol
-> [ExprV Symbol]
-> ExprV Symbol
-> Maybe LocSpecType
-> ExprV Symbol
equationBody Bool
allowTC (Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar Symbol
f) [ExprV Symbol]
xArgs ExprV Symbol
e Maybe LocSpecType
mbT) Sort
t
                      | F.Equ Symbol
f [(Symbol, Sort)]
xts ExprV Symbol
e Sort
t Bool
_ <- [Equation]
axioms
                      , let xArgs :: [ExprV Symbol]
xArgs          = Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar (Symbol -> ExprV Symbol)
-> ((Symbol, Sort) -> Symbol) -> (Symbol, Sort) -> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Sort) -> ExprV Symbol)
-> [(Symbol, Sort)] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
xts
                      , let mbT :: Maybe LocSpecType
mbT            = if [ExprV Symbol] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ExprV Symbol]
xArgs then Maybe LocSpecType
forall a. Maybe a
Nothing else Symbol -> HashMap Symbol LocSpecType -> Maybe LocSpecType
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
f HashMap Symbol LocSpecType
sigs
                   ]
  where
    axioms :: [Equation]
axioms       = GhcSpecRefl -> [Equation]
gsMyAxioms GhcSpecRefl
refl [Equation] -> [Equation] -> [Equation]
forall a. [a] -> [a] -> [a]
++ GhcSpecRefl -> [Equation]
gsImpAxioms GhcSpecRefl
refl
    refl :: GhcSpecRefl
refl         = TargetSpec -> GhcSpecRefl
gsRefl TargetSpec
sp
    sigs :: HashMap Symbol LocSpecType
sigs         = [(Symbol, LocSpecType)] -> HashMap Symbol LocSpecType
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (Var -> Symbol
forall t. NamedThing t => t -> Symbol
GM.simplesymbol Var
v, LocSpecType
t) | (Var
v, LocSpecType
t) <- GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp) ]

equationBody :: Bool -> F.Expr -> [F.Expr] -> F.Expr -> Maybe LocSpecType -> F.Expr
equationBody :: Bool
-> ExprV Symbol
-> [ExprV Symbol]
-> ExprV Symbol
-> Maybe LocSpecType
-> ExprV Symbol
equationBody Bool
allowTC ExprV Symbol
f [ExprV Symbol]
xArgs ExprV Symbol
e Maybe LocSpecType
mbT
  | Just LocSpecType
t <- Maybe LocSpecType
mbT = [ExprV Symbol] -> ExprV Symbol
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
F.pAnd [ExprV Symbol
eBody, LocSpecType -> ExprV Symbol
rBody LocSpecType
t]
  | Bool
otherwise     = ExprV Symbol
eBody
  where
    eBody :: ExprV Symbol
eBody         = Brel -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
F.PAtom Brel
F.Eq (ExprV Symbol -> [ExprV Symbol] -> ExprV Symbol
forall v. ExprV v -> [ExprV v] -> ExprV v
F.eApps ExprV Symbol
f [ExprV Symbol]
xArgs) ExprV Symbol
e
    rBody :: LocSpecType -> ExprV Symbol
rBody LocSpecType
t       = Bool -> [ExprV Symbol] -> ExprV Symbol -> SpecType -> ExprV Symbol
specTypeToLogic Bool
allowTC [ExprV Symbol]
xArgs (ExprV Symbol -> [ExprV Symbol] -> ExprV Symbol
forall v. ExprV v -> [ExprV v] -> ExprV v
F.eApps ExprV Symbol
f [ExprV Symbol]
xArgs) (LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
t)

-- NV Move this to types?
-- sound but imprecise approximation of a type in the logic
specTypeToLogic :: Bool -> [F.Expr] -> F.Expr -> SpecType -> F.Expr
specTypeToLogic :: Bool -> [ExprV Symbol] -> ExprV Symbol -> SpecType -> ExprV Symbol
specTypeToLogic Bool
allowTC [ExprV Symbol]
es ExprV Symbol
expr SpecType
st
  | Bool
ok        = Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
F.subst Subst
su (ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
F.PImp ([ExprV Symbol] -> ExprV Symbol
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
F.pAnd [ExprV Symbol]
args) ExprV Symbol
res)
  | Bool
otherwise = ExprV Symbol
forall v. ExprV v
F.PTrue
  where
    res :: ExprV Symbol
res       = ExprV Symbol -> SpecType -> ExprV Symbol
specTypeToResultRef ExprV Symbol
expr SpecType
st
    args :: [ExprV Symbol]
args      = (ReftV Symbol -> ExprV Symbol -> ExprV Symbol)
-> [ReftV Symbol] -> [ExprV Symbol] -> [ExprV Symbol]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ReftV Symbol -> ExprV Symbol -> ExprV Symbol
forall {v}. Subable (ExprV v) => ReftV v -> ExprV Symbol -> ExprV v
mkExpr (SpecType -> ReftV Symbol
forall {r} {c} {tv}. Reftable r => RType c tv r -> ReftV Symbol
mkReft (SpecType -> ReftV Symbol) -> [SpecType] -> [ReftV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts) [ExprV Symbol]
es
    mkReft :: RType c tv r -> ReftV Symbol
mkReft RType c tv r
t  =  r -> ReftV Symbol
forall r. Reftable r => r -> ReftV Symbol
toReft (r -> ReftV Symbol) -> r -> ReftV Symbol
forall a b. (a -> b) -> a -> b
$ r -> Maybe r -> r
forall a. a -> Maybe a -> a
Mb.fromMaybe r
forall a. Monoid a => a
mempty (RType c tv r -> Maybe r
forall c tv r. RType c tv r -> Maybe r
stripRTypeBase RType c tv r
t)
    mkExpr :: ReftV v -> ExprV Symbol -> ExprV v
mkExpr (F.Reft (Symbol
v, ExprV v
ev)) ExprV Symbol
e = ExprV v -> (Symbol, ExprV Symbol) -> ExprV v
forall a. Subable a => a -> (Symbol, ExprV Symbol) -> a
F.subst1 ExprV v
ev (Symbol
v, ExprV Symbol
e)


    ok :: Bool
ok      = Bool
okLen Bool -> Bool -> Bool
&& Bool
okClass Bool -> Bool -> Bool
&& Bool
okArgs
    okLen :: Bool
okLen   = [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
xs
    okClass :: Bool
okClass = ((Symbol, SpecType) -> Bool) -> [(Symbol, SpecType)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SpecType -> Bool
forall r. Reftable r => r -> Bool
isTauto (SpecType -> Bool)
-> ((Symbol, SpecType) -> SpecType) -> (Symbol, SpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SpecType) -> SpecType
forall a b. (a, b) -> b
snd) [(Symbol, SpecType)]
cls
    okArgs :: Bool
okArgs  = (SpecType -> Bool) -> [SpecType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SpecType -> Bool
forall {v} {c} {tv} {r}.
(Reftable (RTypeV v c tv r), Monoid r) =>
RTypeV v c tv r -> Bool
okArg [SpecType]
ts

    okArg :: RTypeV v c tv r -> Bool
okArg (RVar tv
_ r
_) = Bool
True
    okArg t :: RTypeV v c tv r
t@RApp{}   = RTypeV v c tv r -> Bool
forall r. Reftable r => r -> Bool
isTauto (RTypeV v c tv r
t{rt_reft = mempty})
    okArg RTypeV v c tv r
_          = Bool
False


    su :: Subst
su           = [(Symbol, ExprV Symbol)] -> Subst
F.mkSubst ([(Symbol, ExprV Symbol)] -> Subst)
-> [(Symbol, ExprV Symbol)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [ExprV Symbol] -> [(Symbol, ExprV Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [ExprV Symbol]
es
    ([(Symbol, SpecType)]
cls, [(Symbol, SpecType)]
nocls) = ((Symbol, SpecType) -> Bool)
-> [(Symbol, SpecType)]
-> ([(Symbol, SpecType)], [(Symbol, SpecType)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition ((if Bool
allowTC then SpecType -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isEmbeddedClass else SpecType -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType)(SpecType -> Bool)
-> ((Symbol, SpecType) -> SpecType) -> (Symbol, SpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Symbol, SpecType) -> SpecType
forall a b. (a, b) -> b
snd) ([(Symbol, SpecType)]
 -> ([(Symbol, SpecType)], [(Symbol, SpecType)]))
-> [(Symbol, SpecType)]
-> ([(Symbol, SpecType)], [(Symbol, SpecType)])
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRepV Symbol RTyCon RTyVar RReft -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV Symbol RTyCon RTyVar RReft
trep) (RTypeRepV Symbol RTyCon RTyVar RReft -> [SpecType]
forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_args RTypeRepV Symbol RTyCon RTyVar RReft
trep)
                 :: ([(F.Symbol, SpecType)], [(F.Symbol, SpecType)])
    ([Symbol]
xs, [SpecType]
ts)     = [(Symbol, SpecType)] -> ([Symbol], [SpecType])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Symbol, SpecType)]
nocls :: ([F.Symbol], [SpecType])

    trep :: RTypeRepV Symbol RTyCon RTyVar RReft
trep = SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep SpecType
st


specTypeToResultRef :: F.Expr -> SpecType -> F.Expr
specTypeToResultRef :: ExprV Symbol -> SpecType -> ExprV Symbol
specTypeToResultRef ExprV Symbol
e SpecType
t
  = ReftV Symbol -> ExprV Symbol
forall {v}. Subable (ExprV v) => ReftV v -> ExprV v
mkExpr (ReftV Symbol -> ExprV Symbol) -> ReftV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ RReft -> ReftV Symbol
forall r. Reftable r => r -> ReftV Symbol
toReft (RReft -> ReftV Symbol) -> RReft -> ReftV Symbol
forall a b. (a -> b) -> a -> b
$ RReft -> Maybe RReft -> RReft
forall a. a -> Maybe a -> a
Mb.fromMaybe RReft
forall a. Monoid a => a
mempty (SpecType -> Maybe RReft
forall c tv r. RType c tv r -> Maybe r
stripRTypeBase (SpecType -> Maybe RReft) -> SpecType -> Maybe RReft
forall a b. (a -> b) -> a -> b
$ RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_res RTypeRepV Symbol RTyCon RTyVar RReft
trep)
  where
    mkExpr :: ReftV v -> ExprV v
mkExpr (F.Reft (Symbol
v, ExprV v
ev)) = ExprV v -> (Symbol, ExprV Symbol) -> ExprV v
forall a. Subable a => a -> (Symbol, ExprV Symbol) -> a
F.subst1 ExprV v
ev (Symbol
v, ExprV Symbol
e)
    trep :: RTypeRepV Symbol RTyCon RTyVar RReft
trep                   = SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep SpecType
t