{-# LANGUAGE FlexibleContexts          #-}
module Language.Haskell.Liquid.Constraint.ToFixpoint
  ( cgInfoFInfo
  , fixConfig
  , refinementEQs
  , canRewrite
  ) where

import           Prelude hiding (error)
import qualified Language.Haskell.Liquid.GHC.API as Ghc
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 (coreDeps, dependsOn)
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           Var
import           TyCon                             (TyCon)

import           Language.Haskell.Liquid.Types hiding     ( binds )

fixConfig :: FilePath -> Config -> FC.Config
fixConfig :: FilePath -> Config -> Config
fixConfig FilePath
tgt Config
cfg = Config
forall a. Default a => a
def
  { solver :: SMTSolver
FC.solver                   = Maybe SMTSolver -> SMTSolver
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 (Config -> Bool
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                  = Config -> Bool
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
  , 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 
  , oldPLE :: Bool
FC.oldPLE                   = Config -> Bool
oldPLE Config
cfg
  , maxRWOrderingConstraints :: Maybe Int
FC.maxRWOrderingConstraints = Config -> Maybe Int
maxRWOrderingConstraints Config
cfg
  , rwTerminationCheck :: Bool
FC.rwTerminationCheck       = Config -> Bool
rwTerminationCheck Config
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 (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 { ae :: AxiomEnv
F.ae = AxiomEnv
ax }) FInfo Cinfo
fi
  where
    fi :: FInfo Cinfo
fi               = [SubC Cinfo]
-> [WfC Cinfo]
-> BindEnv
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap Int Cinfo
-> Bool
-> Bool
-> [Triggered Expr]
-> AxiomEnv
-> [DataDecl]
-> [Int]
-> FInfo Cinfo
forall a.
[SubC a]
-> [WfC a]
-> BindEnv
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap Int a
-> Bool
-> Bool
-> [Triggered Expr]
-> AxiomEnv
-> [DataDecl]
-> [Int]
-> GInfo SubC a
F.fi [SubC Cinfo]
cs [WfC Cinfo]
ws BindEnv
bs SEnv Sort
ls SEnv Sort
consts Kuts
ks [Qualifier]
qs HashMap Int Cinfo
bi Bool
aHO Bool
aHOqs [Triggered Expr]
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
bs               = CGInfo -> BindEnv
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 (TargetSpec -> [Equation]
makeEquations 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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` HashSet Var
globalRws) (SubC Cinfo -> Maybe Var
subVar SubC Cinfo
sub)

    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, Hashable 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 (SubC Cinfo -> Maybe Var
subVar SubC Cinfo
sub))

    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
var    <- SubC Cinfo -> Maybe Var
subVar SubC Cinfo
sub
      [Var]
usable <- Var -> HashMap Var [Var] -> Maybe [Var]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Var
var (HashMap Var [Var] -> Maybe [Var])
-> HashMap Var [Var] -> Maybe [Var]
forall a b. (a -> b) -> a -> b
$ GhcSpecRefl -> HashMap Var [Var]
gsRewritesWith (GhcSpecRefl -> HashMap Var [Var])
-> GhcSpecRefl -> HashMap Var [Var]
forall a b. (a -> b) -> a -> b
$ TargetSpec -> GhcSpecRefl
gsRefl TargetSpec
spec
      HashSet Var -> Maybe (HashSet Var)
forall (m :: * -> *) a. Monad m => a -> m a
return (HashSet Var -> Maybe (HashSet Var))
-> HashSet Var -> Maybe (HashSet Var)
forall a b. (a -> b) -> a -> b
$ [Var] -> HashSet Var
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Var]
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 -> Expr -> Expr -> Bool
canRewrite HashSet Symbol
freeVars Expr
from Expr
to = Bool
noFreeSyms Bool -> Bool -> Bool
&& Bool
doesNotDiverge
  where
    fromSyms :: HashSet Symbol
fromSyms           = HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable 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
$ Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms Expr
from)
    toSyms :: HashSet Symbol
toSyms             = HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable 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
$ Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms Expr
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] -> Expr -> Expr -> Maybe Subst
unify (HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
S.toList HashSet Symbol
freeVars) Expr
from Expr
to)
                      Bool -> Bool -> Bool
|| Maybe Subst -> Bool
forall a. Maybe a -> Bool
Mb.isJust ([Symbol] -> Expr -> Expr -> Maybe Subst
unify (HashSet Symbol -> [Symbol]
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 SpecType -> Maybe RReft
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 (Expr -> [Expr]) -> Expr -> [Expr]
forall a b. (a -> b) -> a -> b
$ Reft -> Expr
F.reftPred (RReft -> Reft
forall r. Reftable r => r -> Reft
F.toReft RReft
r) ]
    Maybe RReft
Nothing ->
      []
  where
    tres :: SpecType
tres = RTypeRep RTyCon RTyVar RReft -> SpecType
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 = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (SpecType -> RTypeRep RTyCon RTyVar RReft)
-> SpecType -> RTypeRep 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 | (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 =
         (Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (HashSet Symbol -> Expr -> Expr -> Bool
canRewrite HashSet Symbol
freeVars Expr
lhs Expr
rhs) [()] -> [AutoRewrite] -> [AutoRewrite]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [[SortedReft] -> Expr -> Expr -> AutoRewrite
F.AutoRewrite [SortedReft]
xs Expr
lhs Expr
rhs])
      [AutoRewrite] -> [AutoRewrite] -> [AutoRewrite]
forall a. [a] -> [a] -> [a]
++ (Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (HashSet Symbol -> Expr -> Expr -> Bool
canRewrite HashSet Symbol
freeVars Expr
rhs Expr
lhs) [()] -> [AutoRewrite] -> [AutoRewrite]
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 = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
tRep)

    xs :: [SortedReft]
xs = do
      (Symbol
sym, SpecType
arg) <- [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
tRep) (RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
tRep)
      let e :: Expr
e = Expr -> (RReft -> Expr) -> Maybe RReft -> Expr
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Expr
F.PTrue (Reft -> Expr
F.reftPred (Reft -> Expr) -> (RReft -> Reft) -> RReft -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RReft -> Reft
forall r. Reftable r => r -> Reft
F.toReft) (SpecType -> Maybe RReft
forall c tv r. RType c tv r -> Maybe r
stripRTypeBase SpecType
arg)
      SortedReft -> [SortedReft]
forall (m :: * -> *) a. Monad m => a -> m a
return (SortedReft -> [SortedReft]) -> SortedReft -> [SortedReft]
forall a b. (a -> b) -> a -> b
$ Sort -> Reft -> SortedReft
F.RR (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
rTypeSort TCEmb TyCon
tce SpecType
arg) ((Symbol, Expr) -> Reft
F.Reft (Symbol
sym, Expr
e))
       
    tRep :: RTypeRep RTyCon RTyVar RReft
tRep = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (SpecType -> RTypeRep RTyCon RTyVar RReft)
-> SpecType -> RTypeRep 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) 
                    (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (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 (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (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)
    ([PredType]
ts, PredType
t)   = PredType -> ([PredType], PredType)
Ghc.splitFunTys (PredType -> ([PredType], PredType))
-> (Var -> PredType) -> Var -> ([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.splitForAllTys (PredType -> ([Var], PredType))
-> (Var -> PredType) -> Var -> ([Var], PredType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> PredType
Ghc.varType (Var -> ([PredType], PredType)) -> Var -> ([PredType], PredType)
forall a b. (a -> b) -> a -> b
$ Var
x


doExpand :: TargetSpec -> Config -> F.SubC Cinfo -> Bool
doExpand :: TargetSpec -> Config -> SubC Cinfo -> Bool
doExpand TargetSpec
sp Config
cfg SubC Cinfo
sub = Config -> Bool
Config.allowGlobalPLE Config
cfg
                   Bool -> Bool -> Bool
|| (Config -> Bool
Config.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)] -> Expr -> Sort -> Equation
F.mkEquation (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
f) [(Symbol, Sort)]
xts Expr
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 :: Expr
body           = Expr -> SpecType -> Expr
specTypeToResultRef Expr
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 (RTypeRep RTyCon RTyVar RReft -> SpecType
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           = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
t
    xs :: [Symbol]
xs             = RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
tRep
    ts :: [SpecType]
ts             = RTypeRep RTyCon RTyVar RReft -> [SpecType]
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 (Var -> Expr
forall a. Symbolic a => a -> Expr
F.eVar Var
f) (Symbol -> Expr
F.EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
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
x, SpecType
t)
  | Bool -> Bool
not (Var -> Bool
GM.isDataConId Var
x)
  = [] 
  | Bool
otherwise 
  = Expr -> [Rewrite]
go (Expr -> [Rewrite]) -> Expr -> [Rewrite]
forall a b. (a -> b) -> a -> b
$ Expr -> SpecType -> Expr
specTypeToResultRef (Expr -> [Expr] -> Expr
F.eApps (Symbol -> Expr
F.EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x) (Symbol -> Expr
F.EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds (SpecType -> RTypeRep RTyCon RTyVar RReft
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) = (Expr -> [Rewrite]) -> [Expr] -> [Rewrite]
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
dc) Expr
bd)
      | Brel
eq Brel -> [Brel] -> Bool
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
dc
      , Symbol
dc Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x 
      , (Expr -> Bool) -> [Expr] -> Bool
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 (Expr -> Symbol) -> [Expr] -> [Symbol]
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
dc) Expr
bd)
      | (F.EVar Symbol
dc, [Expr]
xs) <- Expr -> (Expr, [Expr])
F.splitEApp Expr
dc
      , Symbol
dc Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x 
      , (Expr -> Bool) -> [Expr] -> Bool
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 (Expr -> Symbol) -> [Expr] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
xs) Expr
bd]

    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
_ = Maybe SrcSpan -> FilePath -> Symbol
forall a. Maybe SrcSpan -> FilePath -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing FilePath
"makeSimplify.fromEVar"

makeEquations :: TargetSpec -> [F.Equation]
makeEquations :: TargetSpec -> [Equation]
makeEquations TargetSpec
sp = [ Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
F.mkEquation Symbol
f [(Symbol, Sort)]
xts (Expr -> [Expr] -> Expr -> Maybe LocSpecType -> Expr
equationBody (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 (Symbol -> Expr)
-> ((Symbol, Sort) -> Symbol) -> (Symbol, Sort) -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Sort) -> Expr) -> [(Symbol, Sort)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
xts
                      , let mbT :: Maybe LocSpecType
mbT            = if [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Expr]
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 :: F.Expr -> [F.Expr] -> F.Expr -> Maybe LocSpecType -> F.Expr
equationBody :: Expr -> [Expr] -> Expr -> Maybe LocSpecType -> Expr
equationBody 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       = [Expr] -> Expr -> SpecType -> Expr
specTypeToLogic [Expr]
xArgs (Expr -> [Expr] -> Expr
F.eApps Expr
f [Expr]
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 :: [F.Expr] -> F.Expr -> SpecType -> F.Expr
specTypeToLogic :: [Expr] -> Expr -> SpecType -> Expr
specTypeToLogic [Expr]
es Expr
e SpecType
t
  | Bool
ok        = Subst -> Expr -> Expr
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
e SpecType
t
    args :: [Expr]
args      = (Reft -> Expr -> Expr) -> [Reft] -> [Expr] -> [Expr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Reft -> Expr -> Expr
mkExpr (SpecType -> Reft
forall r c tv. Reftable r => RType c tv r -> Reft
mkReft (SpecType -> Reft) -> [SpecType] -> [Reft]
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  =  r -> Reft
forall r. Reftable r => r -> Reft
F.toReft (r -> Reft) -> r -> Reft
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 :: Reft -> Expr -> Expr
mkExpr (F.Reft (Symbol
v, Expr
ev)) Expr
e = Expr -> (Symbol, Expr) -> Expr
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   = [Symbol] -> 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 (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
F.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 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 c
_ [RType c tv r]
_ [RTProp c tv r]
_ r
_) = RType c tv r -> Bool
forall r. Reftable r => r -> Bool
F.isTauto (RType c tv r
t{rt_reft :: r
rt_reft = r
forall a. Monoid a => a
mempty})
    okArg RType c tv r
_                = Bool
False


    su :: Subst
su           = [(Symbol, Expr)] -> Subst
F.mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [Expr]
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 (SpecType -> Bool
forall c t t1. TyConable c => RType 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 (RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
trep) (RTypeRep RTyCon RTyVar RReft -> [SpecType]
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)     = [(Symbol, SpecType)] -> ([Symbol], [SpecType])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Symbol, SpecType)]
nocls :: ([F.Symbol], [SpecType])

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


specTypeToResultRef :: F.Expr -> SpecType -> F.Expr
specTypeToResultRef :: Expr -> SpecType -> Expr
specTypeToResultRef Expr
e SpecType
t
  = Reft -> Expr
mkExpr (Reft -> Expr) -> Reft -> Expr
forall a b. (a -> b) -> a -> b
$ RReft -> Reft
forall r. Reftable r => r -> Reft
F.toReft (RReft -> Reft) -> RReft -> Reft
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
$ RTypeRep RTyCon RTyVar RReft -> SpecType
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)) = Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 Expr
ev (Symbol
v, Expr
e)
    trep :: RTypeRep RTyCon RTyVar RReft
trep                   = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
t