{-# 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 qualified Language.Haskell.Liquid.UX.Config as 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 hiding     ( binds )

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

cgInfoFInfo :: TargetInfo -> CGInfo -> IO (F.FInfo Cinfo)
cgInfoFInfo :: TargetInfo -> CGInfo -> IO (FInfo Cinfo)
cgInfoFInfo TargetInfo
info CGInfo
cgi = 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 = forall a. Monoid a => a -> a -> a
mappend (forall a. Monoid a => a
mempty { ae :: AxiomEnv
F.ae = AxiomEnv
ax }) FInfo Cinfo
fi
  where
    fi :: FInfo Cinfo
fi               = forall a.
[SubC a]
-> [WfC a]
-> BindEnv a
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap Int a
-> Bool
-> Bool
-> [Triggered Expr]
-> AxiomEnv
-> [DataDecl]
-> [Int]
-> GInfo SubC a
F.fi [FixSubC]
cs [FixWfC]
ws FixBindEnv
bs SEnv Sort
ls SEnv Sort
consts Kuts
ks [Qualifier]
qs HashMap Int Cinfo
bi Bool
aHO Bool
aHOqs forall {a}. [a]
es forall a. Monoid a => a
mempty [DataDecl]
adts [Int]
ebs
    cs :: [FixSubC]
cs               = CGInfo -> [FixSubC]
fixCs    CGInfo
cgi
    ws :: [FixWfC]
ws               = CGInfo -> [FixWfC]
fixWfs   CGInfo
cgi
    bs :: FixBindEnv
bs               = CGInfo -> FixBindEnv
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 forall a. Maybe a
Nothing forall a. Maybe a
Nothing) 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            = forall t. HasConfig t => t -> Bool
higherOrderFlag TargetInfo
info
    es :: [a]
es               = [] -- makeAxioms info
    ax :: AxiomEnv
ax               = TargetInfo
-> [(Var, SpecType)] -> HashMap SubcId FixSubC -> AxiomEnv
makeAxiomEnvironment TargetInfo
info (CGInfo -> [(Var, SpecType)]
dataConTys CGInfo
cgi) (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 FixSubC -> AxiomEnv
makeAxiomEnvironment TargetInfo
info [(Var, SpecType)]
xts HashMap SubcId FixSubC
fcs
  = [Equation]
-> [Rewrite]
-> HashMap SubcId Bool
-> HashMap SubcId [AutoRewrite]
-> AxiomEnv
F.AEnv [Equation]
eqs
           (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Var, SpecType) -> [Rewrite]
makeSimplify [(Var, SpecType)]
xts)
           (TargetSpec -> Config -> FixSubC -> Bool
doExpand TargetSpec
sp Config
cfg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap SubcId FixSubC
fcs)
           (TargetInfo -> FixSubC -> [AutoRewrite]
makeRewrites TargetInfo
info forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap SubcId FixSubC
fcs)
  where
    eqs :: [Equation]
eqs      = if Config -> Bool
oldPLE Config
cfg
                then Bool -> TargetSpec -> [Equation]
makeEquations (Config -> Bool
typeclass Config
cfg) TargetSpec
sp forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry 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      = 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 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 -> FixSubC -> [AutoRewrite]
makeRewrites TargetInfo
info FixSubC
sub = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (TCEmb TyCon -> (Var, LocSpecType) -> [AutoRewrite]
makeRewriteOne TCEmb TyCon
tce) forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Var
rws) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs GhcSpecSig
sig
    isGlobalRw :: Bool
isGlobalRw = forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe Bool
False (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 FixSubC -> Maybe Var
subVar FixSubC
sub of
        Just Var
v -> forall a. a -> Maybe a
Just Var
v
        Maybe Var
Nothing ->
          forall a. [a] -> Maybe a
Mb.listToMaybe forall a b. (a -> b) -> a -> b
$ do
            D Int
s Int
e Var
v <- [CoreBind] -> [Def]
coreDefs forall a b. (a -> b) -> a -> b
$ TargetSrc -> [CoreBind]
giCbs forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSrc
giSrc TargetInfo
info
            let (Ghc.RealSrcSpan RealSrcSpan
cc Maybe BufSpan
_) = Cinfo -> SrcSpan
ci_loc forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. TaggedC c a => c a -> a
F.sinfo FixSubC
sub
            forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Int
s forall a. Ord a => a -> a -> Bool
<= RealSrcSpan -> Int
Ghc.srcSpanStartLine RealSrcSpan
cc Bool -> Bool -> Bool
&& Int
e forall a. Ord a => a -> a -> Bool
>= RealSrcSpan -> Int
Ghc.srcSpanEndLine RealSrcSpan
cc
            forall (m :: * -> *) a. Monad m => a -> m a
return Var
v

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

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

    localRws :: HashSet Var
localRws = forall a. a -> Maybe a -> a
Mb.fromMaybe forall a. HashSet a
S.empty forall a b. (a -> b) -> a -> b
$ do
      Var
var    <- Maybe Var
parentFunction
      [Var]
usable <- forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Var
var forall a b. (a -> b) -> a -> b
$ GhcSpecRefl -> HashMap Var [Var]
gsRewritesWith forall a b. (a -> b) -> a -> b
$ TargetSpec -> GhcSpecRefl
gsRefl TargetSpec
spec
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Var]
usable

    globalRws :: HashSet Var
globalRws = forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map forall a. Located a -> a
val forall a b. (a -> b) -> a -> b
$ GhcSpecRefl -> HashSet (Located Var)
gsRewrites 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 -> Expr -> Expr -> Bool
canRewrite HashSet Symbol
freeVars' Expr
from Expr
to = Bool
noFreeSyms Bool -> Bool -> Bool
&& Bool
doesNotDiverge
  where
    fromSyms :: HashSet Symbol
fromSyms           = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.intersection HashSet Symbol
freeVars' (forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall a b. (a -> b) -> a -> b
$ forall a. Subable a => a -> [Symbol]
F.syms Expr
from)
    toSyms :: HashSet Symbol
toSyms             = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.intersection HashSet Symbol
freeVars' (forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall a b. (a -> b) -> a -> b
$ forall a. Subable a => a -> [Symbol]
F.syms Expr
to)
    noFreeSyms :: Bool
noFreeSyms         = forall a. HashSet a -> Bool
S.null forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference HashSet Symbol
toSyms HashSet Symbol
fromSyms
    doesNotDiverge :: Bool
doesNotDiverge     = forall a. Maybe a -> Bool
Mb.isNothing ([Symbol] -> Expr -> Expr -> Maybe Subst
unify (forall a. HashSet a -> [a]
S.toList HashSet Symbol
freeVars') Expr
from Expr
to)
                      Bool -> Bool -> Bool
|| forall a. Maybe a -> Bool
Mb.isJust ([Symbol] -> Expr -> Expr -> Maybe Subst
unify (forall a. HashSet a -> [a]
S.toList HashSet Symbol
freeVars') Expr
to Expr
from)

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

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

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

    xs :: [SortedReft]
xs = do
      (Symbol
sym, SpecType
arg) <- forall a b. [a] -> [b] -> [(a, b)]
zip (forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
tRep) (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
tRep)
      let e :: Expr
e = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Expr
F.PTrue (Reft -> Expr
F.reftPred forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. Reftable r => r -> Reft
F.toReft) (forall c tv r. RType c tv r -> Maybe r
stripRTypeBase SpecType
arg)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort -> Reft -> SortedReft
F.RR (forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce SpecType
arg) ((Symbol, Expr) -> Reft
F.Reft (Symbol
sym, Expr
e))

    tRep :: RTypeRep RTyCon RTyVar RReft
tRep = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
val LocSpecType
t

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


doExpand :: TargetSpec -> Config -> F.SubC Cinfo -> Bool
doExpand :: TargetSpec -> Config -> FixSubC -> Bool
doExpand TargetSpec
sp Config
cfg FixSubC
sub = Config -> Bool
Config.allowGlobalPLE Config
cfg
                   Bool -> Bool -> Bool
|| (Config -> Bool
Config.allowLocalPLE Config
cfg Bool -> Bool -> Bool
&& forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (TargetSpec -> Var -> Bool
isPLEVar TargetSpec
sp) (FixSubC -> Maybe Var
subVar FixSubC
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)] -> Expr -> Sort -> Equation
F.mkEquation (forall a. Symbolic a => a -> Symbol
F.symbol Var
f) [(Symbol, Sort)]
xts Expr
body Sort
tOut
  where
    xts :: [(Symbol, Sort)]
xts            = forall t t1. FilePath -> [t] -> [t1] -> [(t, t1)]
Misc.safeZipWithError FilePath
"specTypeEq" [Symbol]
xs (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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts)
    body :: Expr
body           = Expr -> SpecType -> Expr
specTypeToResultRef Expr
bExp SpecType
t
    tOut :: Sort
tOut           = 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 (forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar RReft
tRep)
    tRep :: RTypeRep RTyCon RTyVar RReft
tRep           = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
t
    xs :: [Symbol]
xs             = forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
tRep
    ts :: [SpecType]
ts             = forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args  RTypeRep RTyCon RTyVar RReft
tRep
    bExp :: Expr
bExp           = Expr -> [Expr] -> Expr
F.eApps (forall a. Symbolic a => a -> Expr
F.eVar Var
f) (Symbol -> Expr
F.EVar 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
  = Expr -> [Rewrite]
go forall a b. (a -> b) -> a -> b
$ Expr -> SpecType -> Expr
specTypeToResultRef (Expr -> [Expr] -> Expr
F.eApps (Symbol -> Expr
F.EVar forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
F.symbol Var
var) (Symbol -> Expr
F.EVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds (forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
t))) SpecType
t
  where
    go :: Expr -> [Rewrite]
go (F.PAnd [Expr]
es) = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Rewrite]
go [Expr]
es

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

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

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

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

    go Expr
_ = []

    isEVar :: Expr -> Bool
isEVar (F.EVar Symbol
_) = Bool
True
    isEVar Expr
_ = Bool
False

    fromEVar :: Expr -> Symbol
fromEVar (F.EVar Symbol
x) = Symbol
x
    fromEVar Expr
_ = forall a. Maybe SrcSpan -> FilePath -> a
impossible 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)] -> Expr -> Sort -> Equation
F.mkEquation Symbol
f [(Symbol, Sort)]
xts (Bool -> Expr -> [Expr] -> Expr -> Maybe LocSpecType -> Expr
equationBody Bool
allowTC (Symbol -> Expr
F.EVar Symbol
f) [Expr]
xArgs Expr
e Maybe LocSpecType
mbT) Sort
t
                      | F.Equ Symbol
f [(Symbol, Sort)]
xts Expr
e Sort
t Bool
_ <- [Equation]
axioms
                      , let xArgs :: [Expr]
xArgs          = Symbol -> Expr
F.EVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
xts
                      , let mbT :: Maybe LocSpecType
mbT            = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Expr]
xArgs then forall a. Maybe a
Nothing else 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 forall a. [a] -> [a] -> [a]
++ GhcSpecRefl -> [Equation]
gsImpAxioms GhcSpecRefl
refl
    refl :: GhcSpecRefl
refl         = TargetSpec -> GhcSpecRefl
gsRefl TargetSpec
sp
    sigs :: HashMap Symbol LocSpecType
sigs         = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (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 -> Expr -> [Expr] -> Expr -> Maybe LocSpecType -> Expr
equationBody Bool
allowTC Expr
f [Expr]
xArgs Expr
e Maybe LocSpecType
mbT
  | Just LocSpecType
t <- Maybe LocSpecType
mbT = [Expr] -> Expr
F.pAnd [Expr
eBody, LocSpecType -> Expr
rBody LocSpecType
t]
  | Bool
otherwise     = Expr
eBody
  where
    eBody :: Expr
eBody         = Brel -> Expr -> Expr -> Expr
F.PAtom Brel
F.Eq (Expr -> [Expr] -> Expr
F.eApps Expr
f [Expr]
xArgs) Expr
e
    rBody :: LocSpecType -> Expr
rBody LocSpecType
t       = Bool -> [Expr] -> Expr -> SpecType -> Expr
specTypeToLogic Bool
allowTC [Expr]
xArgs (Expr -> [Expr] -> Expr
F.eApps Expr
f [Expr]
xArgs) (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 -> [Expr] -> Expr -> SpecType -> Expr
specTypeToLogic Bool
allowTC [Expr]
es Expr
expr SpecType
st
  | Bool
ok        = forall a. Subable a => Subst -> a -> a
F.subst Subst
su (Expr -> Expr -> Expr
F.PImp ([Expr] -> Expr
F.pAnd [Expr]
args) Expr
res)
  | Bool
otherwise = Expr
F.PTrue
  where
    res :: Expr
res       = Expr -> SpecType -> Expr
specTypeToResultRef Expr
expr SpecType
st
    args :: [Expr]
args      = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Reft -> Expr -> Expr
mkExpr (forall {r} {c} {tv}. Reftable r => RType c tv r -> Reft
mkReft forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts) [Expr]
es
    mkReft :: RType c tv r -> Reft
mkReft RType c tv r
t  =  forall r. Reftable r => r -> Reft
F.toReft forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
Mb.fromMaybe forall a. Monoid a => a
mempty (forall c tv r. RType c tv r -> Maybe r
stripRTypeBase RType c tv r
t)
    mkExpr :: Reft -> Expr -> Expr
mkExpr (F.Reft (Symbol
v, Expr
ev)) Expr
e = forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 Expr
ev (Symbol
v, Expr
e)


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

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


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

    trep :: RTypeRep RTyCon RTyVar RReft
trep = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
st


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