{-# 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.HashMap.Strict               as M
import qualified Data.HashSet                      as S
-- import           Language.Fixpoint.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.noStringTheory = not (stringTheory cfg)
  , FC.noslice        = noslice           cfg
  , FC.rewriteAxioms  = allowPLE   cfg
  , FC.pleUndecGuards = pleWithUndecidedGuards cfg
  , FC.etabeta        = etabeta    cfg
  , FC.localRewrites  = dependantCase cfg
  , FC.etaElim        = extensionality cfg
  , FC.extensionality = extensionality    cfg
  , FC.interpreter    = interpreter    cfg
  , FC.rwTermination  = rwTerminationCheck cfg
  , FC.fuel           = fuel      cfg
  , FC.noEnvReduction = not (environmentReduction cfg)
  , FC.inlineANFBinds = inlineANFBindings cfg
  }

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

targetFInfo :: TargetInfo -> CGInfo -> F.FInfo Cinfo
targetFInfo :: TargetInfo -> CGInfo -> GInfo SubC Cinfo
targetFInfo TargetInfo
info CGInfo
cgi = GInfo SubC Cinfo -> GInfo SubC Cinfo -> GInfo SubC Cinfo
forall a. Monoid a => a -> a -> a
mappend (GInfo SubC Cinfo
forall a. Monoid a => a
mempty { F.ae = ax, F.lrws = localRewrites cgi }) GInfo SubC Cinfo
fi
  where
    fi :: GInfo SubC Cinfo
fi               = [SubC Cinfo]
-> [WfC Cinfo]
-> BindEnv Cinfo
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap Int Cinfo
-> Bool
-> Bool
-> [Triggered (ExprBV Symbol Symbol)]
-> AxiomEnv
-> [DataDecl]
-> GInfo SubC Cinfo
forall a.
[SubC a]
-> [WfC a]
-> BindEnv a
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap Int a
-> Bool
-> Bool
-> [Triggered (ExprBV Symbol Symbol)]
-> AxiomEnv
-> [DataDecl]
-> 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 (ExprBV Symbol Symbol)]
forall {a}. [a]
es AxiomEnv
forall a. Monoid a => a
mempty [DataDecl]
adts
    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
    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
    cfg :: Config
cfg              = TargetInfo -> Config
forall t. HasConfig t => t -> Config
getConfig TargetInfo
info
    makeDecls :: Bool
makeDecls        = Config -> Bool
forall t. HasConfig t => t -> Bool
adtFlag Config
cfg
    adts :: [DataDecl]
adts             = if Bool
makeDecls then CGInfo -> [DataDecl]
cgADTs   CGInfo
cgi else [DataDecl]
forall a. Monoid a => a
mempty
    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) (GInfo SubC Cinfo -> HashMap SubcId (SubC Cinfo)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm GInfo SubC 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      = [Equation]
axioms
    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. 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. 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. 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 => (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
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol -> Bool
canRewrite HashSet Symbol
freeVars' ExprBV Symbol Symbol
from ExprBV Symbol 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. Hashable a => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ ExprBV Symbol Symbol -> [Variable (ExprBV Symbol Symbol)]
forall a. Subable a => a -> [Variable a]
F.syms ExprBV Symbol 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. Hashable a => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ ExprBV Symbol Symbol -> [Variable (ExprBV Symbol Symbol)]
forall a. Subable a => a -> [Variable a]
F.syms ExprBV Symbol 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. 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]
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol -> Maybe Subst
unify (HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
S.toList HashSet Symbol
freeVars') ExprBV Symbol Symbol
from ExprBV Symbol Symbol
to)
                      Bool -> Bool -> Bool
|| Maybe Subst -> Bool
forall a. Maybe a -> Bool
Mb.isJust ([Symbol]
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol -> Maybe Subst
unify (HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
S.toList HashSet Symbol
freeVars') ExprBV Symbol Symbol
to ExprBV Symbol Symbol
from)

refinementEQs :: LocSpecType -> [(F.Expr, F.Expr)]
refinementEQs :: LocSpecType -> [(ExprBV Symbol Symbol, ExprBV Symbol Symbol)]
refinementEQs LocSpecType
t =
  case SpecType -> Maybe RReft
forall b v c tv r. RTypeBV b v c tv r -> Maybe r
stripRTypeBase SpecType
tres of
    Just RReft
r ->
      [ (ExprBV Symbol Symbol
lhs, ExprBV Symbol Symbol
rhs) | (F.EEq ExprBV Symbol Symbol
lhs ExprBV Symbol Symbol
rhs) <- ExprBV Symbol Symbol -> [ExprBV Symbol Symbol]
F.splitPAnd (ExprBV Symbol Symbol -> [ExprBV Symbol Symbol])
-> ExprBV Symbol Symbol -> [ExprBV Symbol Symbol]
forall a b. (a -> b) -> a -> b
$ ReftBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ReftBV b v -> ExprBV b v
F.reftPred (RReft -> ReftBV (ReftBind RReft) (ReftVar RReft)
forall r. ToReft r => r -> ReftBV (ReftBind r) (ReftVar r)
toReft RReft
r) ]
    Maybe RReft
Nothing ->
      []
  where
    tres :: SpecType
tres = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> SpecType
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
ty_res RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
tRep
    tRep :: RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
tRep = SpecType -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep (SpecType -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft)
-> SpecType -> RTypeRepBV Symbol 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 | (ExprBV Symbol Symbol
lhs, ExprBV Symbol Symbol
rhs) <- LocSpecType -> [(ExprBV Symbol Symbol, ExprBV Symbol Symbol)]
refinementEQs LocSpecType
t , AutoRewrite
rw <- ExprBV Symbol Symbol -> ExprBV Symbol Symbol -> [AutoRewrite]
rewrites ExprBV Symbol Symbol
lhs ExprBV Symbol Symbol
rhs ]
  where

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

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

    xs :: [SortedReft]
xs = do
      (sym, arg) <- [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [Symbol]
forall b v c tv r. RTypeRepBV b v c tv r -> [b]
ty_binds RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
tRep) (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [SpecType]
forall b v c tv r. RTypeRepBV b v c tv r -> [RTypeBV b v c tv r]
ty_args RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
tRep)
      let e = ExprBV Symbol Symbol
-> (RReft -> ExprBV Symbol Symbol)
-> Maybe RReft
-> ExprBV Symbol Symbol
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ExprBV Symbol Symbol
forall b v. ExprBV b v
F.PTrue (ReftBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ReftBV b v -> ExprBV b v
F.reftPred (ReftBV Symbol Symbol -> ExprBV Symbol Symbol)
-> (RReft -> ReftBV Symbol Symbol) -> RReft -> ExprBV Symbol Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RReft -> ReftBV Symbol Symbol
RReft -> ReftBV (ReftBind RReft) (ReftVar RReft)
forall r. ToReft r => r -> ReftBV (ReftBind r) (ReftVar r)
toReft) (SpecType -> Maybe RReft
forall b v c tv r. RTypeBV b v c tv r -> Maybe r
stripRTypeBase SpecType
arg)
      return $ F.RR (RT.rTypeSort tce arg) (F.Reft (sym, e))

    tRep :: RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
tRep = SpecType -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep (SpecType -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft)
-> SpecType -> RTypeRepBV Symbol 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
&& (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
Ghc.isClassPred (Type
tType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
ts'))
  where
    msg :: FilePath
msg       = FilePath
"hasClassArg: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Var, [Type]) -> FilePath
forall a. PPrint a => a -> FilePath
showpp (Var
x, Type
tType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
ts')
    ([Scaled Type]
ts, Type
t)   = Type -> ([Scaled Type], Type)
Ghc.splitFunTys (Type -> ([Scaled Type], Type))
-> (Var -> Type) -> Var -> ([Scaled Type], Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Var], Type) -> Type
forall a b. (a, b) -> b
snd (([Var], Type) -> Type) -> (Var -> ([Var], Type)) -> Var -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ([Var], Type)
Ghc.splitForAllTyCoVars (Type -> ([Var], Type)) -> (Var -> Type) -> Var -> ([Var], Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Type
Ghc.varType (Var -> ([Scaled Type], Type)) -> Var -> ([Scaled Type], Type)
forall a b. (a -> b) -> a -> b
$ Var
x
    ts' :: [Type]
ts'       = (Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
Ghc.irrelevantMult [Scaled Type]
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...

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
  = ExprBV Symbol Symbol -> [Rewrite]
go (ExprBV Symbol Symbol -> [Rewrite])
-> ExprBV Symbol Symbol -> [Rewrite]
forall a b. (a -> b) -> a -> b
$ ExprBV Symbol Symbol -> SpecType -> ExprBV Symbol Symbol
specTypeToResultRef (ExprBV Symbol Symbol
-> [ExprBV Symbol Symbol] -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> [ExprBV b v] -> ExprBV b v
F.eApps (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar (Symbol -> ExprBV Symbol Symbol) -> Symbol -> ExprBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
var) (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar (Symbol -> ExprBV Symbol Symbol)
-> [Symbol] -> [ExprBV Symbol Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [Symbol]
forall b v c tv r. RTypeRepBV b v c tv r -> [b]
ty_binds (SpecType -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep SpecType
t))) SpecType
t
  where
    go :: ExprBV Symbol Symbol -> [Rewrite]
go (F.PAnd [ExprBV Symbol Symbol]
es) = (ExprBV Symbol Symbol -> [Rewrite])
-> [ExprBV Symbol Symbol] -> [Rewrite]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ExprBV Symbol Symbol -> [Rewrite]
go [ExprBV Symbol Symbol]
es

    go (F.PAtom Brel
eq (F.EApp (F.EVar Symbol
f) ExprBV Symbol Symbol
expr) ExprBV Symbol 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, [ExprBV Symbol Symbol]
xs) <- ExprBV Symbol Symbol
-> (ExprBV Symbol Symbol, [ExprBV Symbol Symbol])
forall b v. ExprBV b v -> (ExprBV b v, [ExprBV b v])
F.splitEApp ExprBV Symbol 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
      , (ExprBV Symbol Symbol -> Bool) -> [ExprBV Symbol Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ExprBV Symbol Symbol -> Bool
forall {b} {v}. ExprBV b v -> Bool
isEVar [ExprBV Symbol Symbol]
xs
      = [Symbol -> Symbol -> [Symbol] -> ExprBV Symbol Symbol -> Rewrite
F.SMeasure Symbol
f Symbol
dc (ExprBV Symbol Symbol -> Symbol
forall {b} {v}. ExprBV b v -> v
fromEVar (ExprBV Symbol Symbol -> Symbol)
-> [ExprBV Symbol Symbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprBV Symbol Symbol]
xs) ExprBV Symbol Symbol
bd]

    go (F.PIff (F.EApp (F.EVar Symbol
f) ExprBV Symbol Symbol
expr) ExprBV Symbol Symbol
bd)
      | (F.EVar Symbol
dc, [ExprBV Symbol Symbol]
xs) <- ExprBV Symbol Symbol
-> (ExprBV Symbol Symbol, [ExprBV Symbol Symbol])
forall b v. ExprBV b v -> (ExprBV b v, [ExprBV b v])
F.splitEApp ExprBV Symbol 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
      , (ExprBV Symbol Symbol -> Bool) -> [ExprBV Symbol Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ExprBV Symbol Symbol -> Bool
forall {b} {v}. ExprBV b v -> Bool
isEVar [ExprBV Symbol Symbol]
xs
      = [Symbol -> Symbol -> [Symbol] -> ExprBV Symbol Symbol -> Rewrite
F.SMeasure Symbol
f Symbol
dc (ExprBV Symbol Symbol -> Symbol
forall {b} {v}. ExprBV b v -> v
fromEVar (ExprBV Symbol Symbol -> Symbol)
-> [ExprBV Symbol Symbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprBV Symbol Symbol]
xs) ExprBV Symbol Symbol
bd]

    go (F.EApp (F.EVar Symbol
f) ExprBV Symbol Symbol
expr)
      | (F.EVar Symbol
dc, [ExprBV Symbol Symbol]
xs) <- ExprBV Symbol Symbol
-> (ExprBV Symbol Symbol, [ExprBV Symbol Symbol])
forall b v. ExprBV b v -> (ExprBV b v, [ExprBV b v])
F.splitEApp ExprBV Symbol 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
      , (ExprBV Symbol Symbol -> Bool) -> [ExprBV Symbol Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ExprBV Symbol Symbol -> Bool
forall {b} {v}. ExprBV b v -> Bool
isEVar [ExprBV Symbol Symbol]
xs
      = [Symbol -> Symbol -> [Symbol] -> ExprBV Symbol Symbol -> Rewrite
F.SMeasure Symbol
f Symbol
dc (ExprBV Symbol Symbol -> Symbol
forall {b} {v}. ExprBV b v -> v
fromEVar (ExprBV Symbol Symbol -> Symbol)
-> [ExprBV Symbol Symbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprBV Symbol Symbol]
xs) ExprBV Symbol Symbol
forall b v. ExprBV b v
F.PTrue]

    go (F.PNot (F.EApp (F.EVar Symbol
f) ExprBV Symbol Symbol
expr))
      | (F.EVar Symbol
dc, [ExprBV Symbol Symbol]
xs) <- ExprBV Symbol Symbol
-> (ExprBV Symbol Symbol, [ExprBV Symbol Symbol])
forall b v. ExprBV b v -> (ExprBV b v, [ExprBV b v])
F.splitEApp ExprBV Symbol 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
      , (ExprBV Symbol Symbol -> Bool) -> [ExprBV Symbol Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ExprBV Symbol Symbol -> Bool
forall {b} {v}. ExprBV b v -> Bool
isEVar [ExprBV Symbol Symbol]
xs
      = [Symbol -> Symbol -> [Symbol] -> ExprBV Symbol Symbol -> Rewrite
F.SMeasure Symbol
f Symbol
dc (ExprBV Symbol Symbol -> Symbol
forall {b} {v}. ExprBV b v -> v
fromEVar (ExprBV Symbol Symbol -> Symbol)
-> [ExprBV Symbol Symbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprBV Symbol Symbol]
xs) ExprBV Symbol Symbol
forall b v. ExprBV b v
F.PFalse]

    go ExprBV Symbol Symbol
_ = []

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

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

specTypeToResultRef :: F.Expr -> SpecType -> F.Expr
specTypeToResultRef :: ExprBV Symbol Symbol -> SpecType -> ExprBV Symbol Symbol
specTypeToResultRef ExprBV Symbol Symbol
e SpecType
t
  = ReftBV Symbol Symbol -> ExprBV Symbol Symbol
forall {v}.
(Variable (ExprBV Symbol v) ~ Symbol, Subable (ExprBV Symbol v)) =>
ReftBV Symbol v -> ExprBV Symbol v
mkExpr (ReftBV Symbol Symbol -> ExprBV Symbol Symbol)
-> ReftBV Symbol Symbol -> ExprBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ RReft -> ReftBV (ReftBind RReft) (ReftVar RReft)
forall r. ToReft r => r -> ReftBV (ReftBind r) (ReftVar r)
toReft (RReft -> ReftBV (ReftBind RReft) (ReftVar RReft))
-> RReft -> ReftBV (ReftBind RReft) (ReftVar RReft)
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 b v c tv r. RTypeBV b v c tv r -> Maybe r
stripRTypeBase (SpecType -> Maybe RReft) -> SpecType -> Maybe RReft
forall a b. (a -> b) -> a -> b
$ RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> SpecType
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
ty_res RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep)
  where
    mkExpr :: ReftBV Symbol v -> ExprBV Symbol v
mkExpr (F.Reft (Symbol
v, ExprBV Symbol v
ev)) = ExprBV Symbol v
-> (Variable (ExprBV Symbol v),
    ExprBV (Variable (ExprBV Symbol v)) (Variable (ExprBV Symbol v)))
-> ExprBV Symbol v
forall a.
Subable a =>
a -> (Variable a, ExprBV (Variable a) (Variable a)) -> a
F.subst1 ExprBV Symbol v
ev (Symbol
Variable (ExprBV Symbol v)
v, ExprBV Symbol Symbol
ExprBV (Variable (ExprBV Symbol v)) (Variable (ExprBV Symbol v))
e)
    trep :: RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep                   = SpecType -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep SpecType
t