{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections     #-}
{-# LANGUAGE TypeOperators     #-}
{-# LANGUAGE BangPatterns      #-}

-- | This module contains the functions related to @Error@ type,
-- in particular, to @tidyError@ using a solution, and @pprint@ errors.

module Language.Haskell.Liquid.UX.Errors ( tidyError ) where

import           Control.Arrow                       (second)
import           Data.Either                         (partitionEithers)
import qualified Data.HashMap.Strict                 as M
import qualified Data.HashSet                        as S
import qualified Data.List                           as L
import           Data.Hashable
import           Data.Maybe                          (maybeToList)
import qualified Language.Fixpoint.Types             as F
import qualified Language.Fixpoint.Solver.EnvironmentReduction as F
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Transforms.Simplify
import           Language.Haskell.Liquid.UX.Config
import           Language.Haskell.Liquid.UX.Tidy
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Types
import qualified Language.Haskell.Liquid.GHC.Misc    as GM
import qualified Language.Haskell.Liquid.Misc        as Misc

-- import Debug.Trace

type Ctx  = M.HashMap F.Symbol SpecType
type CtxM = M.HashMap F.Symbol (WithModel SpecType)

------------------------------------------------------------------------
tidyError :: Config -> Error -> Error
------------------------------------------------------------------------
tidyError :: Config -> Error -> Error
tidyError Config
cfg
  = (SpecType -> SpecType) -> Error -> Error
forall a b. (a -> b) -> TError a -> TError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Tidy -> SpecType -> SpecType
tidySpecType Tidy
tidy)
  (Error -> Error) -> (Error -> Error) -> Error -> Error
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy -> Error -> Error
tidyErrContext Tidy
tidy
  where
    tidy :: Tidy
tidy = Config -> Tidy
configTidy Config
cfg

configTidy :: Config -> F.Tidy
configTidy :: Config -> Tidy
configTidy Config
cfg
  | Config -> Bool
shortNames Config
cfg = Tidy
F.Lossy
  | Bool
otherwise      = Tidy
F.Full

tidyErrContext :: F.Tidy -> Error -> Error
tidyErrContext :: Tidy -> Error -> Error
tidyErrContext Tidy
k e :: Error
e@(ErrSubType {})
  = Error
e { ctx = c', tact = F.subst θ tA, texp = F.subst θ tE }
    where
      (SubstV Symbol
θ, Ctx
c') = Tidy -> [Symbol] -> Ctx -> (SubstV Symbol, Ctx)
tidyCtx Tidy
k [Symbol]
xs (Error -> Ctx
forall t. TError t -> HashMap Symbol t
ctx Error
e)
      xs :: [Symbol]
xs      = SpecType -> [Variable SpecType]
forall a. Subable a => a -> [Variable a]
F.syms SpecType
tA [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Variable SpecType]
forall a. Subable a => a -> [Variable a]
F.syms SpecType
tE
      tA :: SpecType
tA      = Error -> SpecType
forall t. TError t -> t
tact Error
e
      tE :: SpecType
tE      = Error -> SpecType
forall t. TError t -> t
texp Error
e

tidyErrContext Tidy
_ e :: Error
e@(ErrSubTypeModel {})
  = Error
e { ctxM = c', tactM = fmap (F.subst θ) tA, texp = fmap (F.subst θ) tE }
    where
      (SubstV Symbol
θ, CtxM
c') = [Symbol] -> CtxM -> (SubstV Symbol, CtxM)
tidyCtxM [Symbol]
xs (CtxM -> (SubstV Symbol, CtxM)) -> CtxM -> (SubstV Symbol, CtxM)
forall a b. (a -> b) -> a -> b
$ Error -> CtxM
forall t. TError t -> HashMap Symbol (WithModel t)
ctxM Error
e
      xs :: [Symbol]
xs      = WithModel SpecType -> [Variable (WithModel SpecType)]
forall a. Subable a => a -> [Variable a]
F.syms WithModel SpecType
tA [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Variable SpecType]
forall a. Subable a => a -> [Variable a]
F.syms SpecType
tE
      tA :: WithModel SpecType
tA      = Error -> WithModel SpecType
forall t. TError t -> WithModel t
tactM Error
e
      tE :: SpecType
tE      = Error -> SpecType
forall t. TError t -> t
texp Error
e

tidyErrContext Tidy
k e :: Error
e@(ErrAssType {})
  = Error
e { ctx = c', cond = F.subst θ p }
    where
      m :: Ctx
m       = Error -> Ctx
forall t. TError t -> HashMap Symbol t
ctx Error
e
      (SubstV Symbol
θ, Ctx
c') = Tidy -> [Symbol] -> Ctx -> (SubstV Symbol, Ctx)
tidyCtx Tidy
k [Symbol]
xs Ctx
m
      xs :: [Variable SpecType]
xs      = SpecType -> [Variable SpecType]
forall a. Subable a => a -> [Variable a]
F.syms SpecType
p
      p :: SpecType
p       = Error -> SpecType
forall t. TError t -> t
cond Error
e

tidyErrContext Tidy
_ Error
e
  = Error
e

--------------------------------------------------------------------------------
tidyCtx       :: F.Tidy -> [F.Symbol] -> Ctx -> (F.Subst, Ctx)
--------------------------------------------------------------------------------
tidyCtx :: Tidy -> [Symbol] -> Ctx -> (SubstV Symbol, Ctx)
tidyCtx Tidy
k [Symbol]
xs Ctx
m = (SubstV Symbol
θ1 SubstV Symbol -> SubstV Symbol -> SubstV Symbol
forall a. Monoid a => a -> a -> a
`mappend` SubstV Symbol
θ2, [(Symbol, SpecType)] -> Ctx
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [(Symbol, SpecType)]
yts)
  where
    yts :: [(Symbol, SpecType)]
yts        = [Symbol -> SpecType -> (Symbol, SpecType)
forall {f :: * -> *} {c} {tv}.
(Variable (f (ReftBV Symbol Symbol)) ~ Symbol,
 ReftBind (f (ReftBV Symbol Symbol)) ~ Symbol, TyConable c,
 IsReft (f (ReftBV Symbol Symbol)), Functor f,
 Subable (f (ReftBV Symbol Symbol))) =>
Symbol
-> RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol))
-> (Symbol, RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol)))
tBind Symbol
x (Tidy -> SpecType -> SpecType
tidySpecType Tidy
k SpecType
t) | (Symbol
x, SpecType
t) <- [(Symbol, SpecType)]
xt2s]
    (SubstV Symbol
θ2, [(Symbol, SpecType)]
xt2s) = [(Symbol, SpecType)] -> (SubstV Symbol, [(Symbol, SpecType)])
tidyREnv [(Symbol, SpecType)]
xt1s
    (SubstV Symbol
θ1, [(Symbol, SpecType)]
xt1s) = [(Symbol, SpecType)] -> (SubstV Symbol, [(Symbol, SpecType)])
forall t.
(Subable t, Variable t ~ Symbol) =>
[(Symbol, t)] -> (SubstV Symbol, [(Symbol, t)])
tidyTemps [(Symbol, SpecType)]
xts
    xts :: [(Symbol, SpecType)]
xts        = [Symbol] -> Ctx -> [(Symbol, SpecType)]
sliceREnv [Symbol]
xs Ctx
m
    tBind :: Symbol
-> RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol))
-> (Symbol, RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol)))
tBind Symbol
x RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol))
t  = (Symbol
x', RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol))
-> Symbol -> RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol))
forall c (f :: * -> *) tv.
(TyConable c, IsReft (f (ReftBV Symbol Symbol)), Functor f,
 Subable (f (ReftBV Symbol Symbol)),
 Variable (f (ReftBV Symbol Symbol))
 ~ Variable (ReftBV Symbol Symbol),
 ReftBind (f (ReftBV Symbol Symbol))
 ~ ReftBind (ReftBV Symbol Symbol)) =>
RType c tv (f (ReftBV Symbol Symbol))
-> Symbol -> RType c tv (f (ReftBV Symbol Symbol))
shiftVV RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol))
t Symbol
x') where x' :: Symbol
x' = Symbol -> Symbol
F.tidySymbol Symbol
x

tidyCtxM       :: [F.Symbol] -> CtxM -> (F.Subst, CtxM)
tidyCtxM :: [Symbol] -> CtxM -> (SubstV Symbol, CtxM)
tidyCtxM [Symbol]
xs CtxM
m  = (SubstV Symbol
θ, [(Symbol, WithModel SpecType)] -> CtxM
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [(Symbol, WithModel SpecType)]
yts)
  where
    yts :: [(Symbol, WithModel SpecType)]
yts       = [Symbol -> WithModel SpecType -> (Symbol, WithModel SpecType)
forall {f :: * -> *} {c} {f :: * -> *} {tv}.
(Variable (f (ReftBV Symbol Symbol)) ~ Symbol,
 ReftBind (f (ReftBV Symbol Symbol)) ~ Symbol, TyConable c,
 IsReft (f (ReftBV Symbol Symbol)), Functor f, Functor f,
 Subable (f (ReftBV Symbol Symbol))) =>
Symbol
-> f (RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol)))
-> (Symbol,
    f (RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol))))
tBind Symbol
x WithModel SpecType
t | (Symbol
x, WithModel SpecType
t) <- [(Symbol, WithModel SpecType)]
xts]
    (SubstV Symbol
θ, [(Symbol, WithModel SpecType)]
xts)  = [(Symbol, WithModel SpecType)]
-> (SubstV Symbol, [(Symbol, WithModel SpecType)])
forall t.
(Subable t, Variable t ~ Symbol) =>
[(Symbol, t)] -> (SubstV Symbol, [(Symbol, t)])
tidyTemps ([(Symbol, WithModel SpecType)]
 -> (SubstV Symbol, [(Symbol, WithModel SpecType)]))
-> [(Symbol, WithModel SpecType)]
-> (SubstV Symbol, [(Symbol, WithModel SpecType)])
forall a b. (a -> b) -> a -> b
$ (WithModel SpecType -> WithModel SpecType)
-> (Symbol, WithModel SpecType) -> (Symbol, WithModel SpecType)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((SpecType -> SpecType) -> WithModel SpecType -> WithModel SpecType
forall a b. (a -> b) -> WithModel a -> WithModel b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SpecType -> SpecType
stripReft) ((Symbol, WithModel SpecType) -> (Symbol, WithModel SpecType))
-> [(Symbol, WithModel SpecType)] -> [(Symbol, WithModel SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> CtxM -> [(Symbol, WithModel SpecType)]
tidyREnvM [Symbol]
xs CtxM
m
    tBind :: Symbol
-> f (RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol)))
-> (Symbol,
    f (RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol))))
tBind Symbol
x f (RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol)))
t = (Symbol
x', (RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol))
 -> RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol)))
-> f (RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol)))
-> f (RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol)))
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol))
-> Symbol -> RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol))
forall c (f :: * -> *) tv.
(TyConable c, IsReft (f (ReftBV Symbol Symbol)), Functor f,
 Subable (f (ReftBV Symbol Symbol)),
 Variable (f (ReftBV Symbol Symbol))
 ~ Variable (ReftBV Symbol Symbol),
 ReftBind (f (ReftBV Symbol Symbol))
 ~ ReftBind (ReftBV Symbol Symbol)) =>
RType c tv (f (ReftBV Symbol Symbol))
-> Symbol -> RType c tv (f (ReftBV Symbol Symbol))
`shiftVV` Symbol
x') f (RTypeBV Symbol Symbol c tv (f (ReftBV Symbol Symbol)))
t) where x' :: Symbol
x' = Symbol -> Symbol
F.tidySymbol Symbol
x

tidyREnv :: [(F.Symbol, SpecType)] -> (F.Subst, [(F.Symbol, SpecType)])
tidyREnv :: [(Symbol, SpecType)] -> (SubstV Symbol, [(Symbol, SpecType)])
tidyREnv [(Symbol, SpecType)]
xts    = (SubstV Symbol
θ, (SpecType -> SpecType) -> (Symbol, SpecType) -> (Symbol, SpecType)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (SubstV (Variable SpecType) -> SpecType -> SpecType
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV Symbol
SubstV (Variable SpecType)
θ) ((Symbol, SpecType) -> (Symbol, SpecType))
-> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SpecType)]
zts)
  where
    θ :: SubstV Symbol
θ           = [(Symbol, Expr)] -> SubstV Symbol
expandVarDefs [(Symbol, Expr)]
yes
    ([(Symbol, Expr)]
yes, [(Symbol, SpecType)]
zts)  = [Either (Symbol, Expr) (Symbol, SpecType)]
-> ([(Symbol, Expr)], [(Symbol, SpecType)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either (Symbol, Expr) (Symbol, SpecType)]
 -> ([(Symbol, Expr)], [(Symbol, SpecType)]))
-> [Either (Symbol, Expr) (Symbol, SpecType)]
-> ([(Symbol, Expr)], [(Symbol, SpecType)])
forall a b. (a -> b) -> a -> b
$ ((Symbol, SpecType) -> Either (Symbol, Expr) (Symbol, SpecType))
-> [(Symbol, SpecType)]
-> [Either (Symbol, Expr) (Symbol, SpecType)]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, SpecType) -> Either (Symbol, Expr) (Symbol, SpecType)
forall a. (a, SpecType) -> Either (a, Expr) (a, SpecType)
isInline [(Symbol, SpecType)]
xts

-- | 'expandVarDefs [(x1, e1), ... ,(xn, en)] returns a `Subst` that
--   contains the fully substituted definitions for each `xi`. For example,
--      expandVarDefs [(x1, 'x2 + x3'), (x5, 'x1 + 1')]
--   should return
--     [x1 := 'x2 + x3, x5 := (x2 + x3) + 1]

expandVarDefs :: [(F.Symbol, F.Expr)] -> F.Subst
expandVarDefs :: [(Symbol, Expr)] -> SubstV Symbol
expandVarDefs      = SubstV Symbol -> [(Symbol, Expr)] -> SubstV Symbol
forall {v}. Hashable v => SubstV v -> [(v, ExprBV v v)] -> SubstV v
go SubstV Symbol
forall a. Monoid a => a
mempty
  where
    go :: SubstV v -> [(v, ExprBV v v)] -> SubstV v
go !SubstV v
su [(Variable (ExprBV v v), ExprBV v v)]
xes
      | [(v, ExprBV v v)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(v, ExprBV v v)]
[(Variable (ExprBV v v), ExprBV v v)]
yes   = SubstV v
su SubstV v -> SubstV v -> SubstV v
forall a. Monoid a => a -> a -> a
`mappend` [(v, ExprBV v v)] -> SubstV v
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst [(v, ExprBV v v)]
[(Variable (ExprBV v v), ExprBV v v)]
xes
      | Bool
otherwise  = SubstV v -> [(v, ExprBV v v)] -> SubstV v
go (SubstV v
su SubstV v -> SubstV v -> SubstV v
forall a. Monoid a => a -> a -> a
`mappend` SubstV v
SubstV (Variable (ExprBV v v))
su') [(v, ExprBV v v)]
[(Variable (ExprBV v v), ExprBV v v)]
xes''
      where
       xes'' :: [(Variable (ExprBV v v), ExprBV v v)]
xes''       = [(Variable (ExprBV v v)
z, SubstV (Variable (ExprBV v v)) -> ExprBV v v -> ExprBV v v
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV (Variable (ExprBV v v))
su' ExprBV v v
e) | (Variable (ExprBV v v)
z, ExprBV v v
e) <- [(Variable (ExprBV v v), ExprBV v v)]
zes]
       xs :: HashSet (Variable (ExprBV v v))
xs          = [Variable (ExprBV v v)] -> HashSet (Variable (ExprBV v v))
forall a. Hashable a => [a] -> HashSet a
S.fromList [Variable (ExprBV v v)
x | (Variable (ExprBV v v)
x, ExprBV v v
_) <- [(Variable (ExprBV v v), ExprBV v v)]
xes]
       su' :: SubstV (Variable (ExprBV v v))
su'         = [(Variable (ExprBV v v),
  ExprBV (Variable (ExprBV v v)) (Variable (ExprBV v v)))]
-> SubstV (Variable (ExprBV v v))
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst [(Variable (ExprBV v v), ExprBV v v)]
[(Variable (ExprBV v v),
  ExprBV (Variable (ExprBV v v)) (Variable (ExprBV v v)))]
yes
       ([(Variable (ExprBV v v), ExprBV v v)]
yes, [(Variable (ExprBV v v), ExprBV v v)]
zes)  = ((Variable (ExprBV v v), ExprBV v v) -> Bool)
-> [(Variable (ExprBV v v), ExprBV v v)]
-> ([(Variable (ExprBV v v), ExprBV v v)],
    [(Variable (ExprBV v v), ExprBV v v)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (HashSet (Variable (ExprBV v v)) -> ExprBV v v -> Bool
forall {a}. Subable a => HashSet (Variable a) -> a -> Bool
isDef HashSet (Variable (ExprBV v v))
xs (ExprBV v v -> Bool)
-> ((Variable (ExprBV v v), ExprBV v v) -> ExprBV v v)
-> (Variable (ExprBV v v), ExprBV v v)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Variable (ExprBV v v), ExprBV v v) -> ExprBV v v
forall a b. (a, b) -> b
snd) [(Variable (ExprBV v v), ExprBV v v)]
xes
    isDef :: HashSet (Variable a) -> a -> Bool
isDef HashSet (Variable a)
xs a
e     = Bool -> Bool
not ((Variable a -> Bool) -> [Variable a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Variable a -> HashSet (Variable a) -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
`S.member` HashSet (Variable a)
xs) (a -> [Variable a]
forall a. Subable a => a -> [Variable a]
F.syms a
e))

isInline :: (a, SpecType) -> Either (a, F.Expr) (a, SpecType)
isInline :: forall a. (a, SpecType) -> Either (a, Expr) (a, SpecType)
isInline (a
x, SpecType
t) =
    (Expr -> Either (a, Expr) (a, SpecType))
-> (SpecType -> Either (a, Expr) (a, SpecType))
-> Either Expr SpecType
-> Either (a, Expr) (a, SpecType)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((a, Expr) -> Either (a, Expr) (a, SpecType)
forall a b. a -> Either a b
Left ((a, Expr) -> Either (a, Expr) (a, SpecType))
-> (Expr -> (a, Expr)) -> Expr -> Either (a, Expr) (a, SpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
x,)) ((a, SpecType) -> Either (a, Expr) (a, SpecType)
forall a b. b -> Either a b
Right ((a, SpecType) -> Either (a, Expr) (a, SpecType))
-> (SpecType -> (a, SpecType))
-> SpecType
-> Either (a, Expr) (a, SpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
x,)) (SpecType -> Either Expr SpecType
isInline' SpecType
t')
  where
    -- tidyInternalRefas could drop some conjuncts which affects whether
    -- bindings are eliminated in isInline'
    t' :: SpecType
t' = SpecType -> SpecType
tidyInternalRefas SpecType
t

isInline' :: SpecType -> Either F.Expr SpecType
isInline' :: SpecType -> Either Expr SpecType
isInline' SpecType
t = case Maybe RReft
ro of
                Maybe RReft
Nothing -> SpecType -> Either Expr SpecType
forall a b. b -> Either a b
Right SpecType
t'
                Just RReft
rr -> case ReftBV Symbol Symbol -> Maybe Expr
F.isSingletonReft (RReft -> ReftBV Symbol Symbol
forall b v r. UReftBV b v r -> r
ur_reft RReft
rr) of
                  Just Expr
e -- Treat as singleton only if there aren't other conjucts
                    | [Expr
_] <- Expr -> [Expr]
forall b v. (Eq b, Eq v) => ExprBV b v -> [ExprBV b v]
F.conjuncts (ReftBV Symbol Symbol -> Expr
forall b v. ReftBV b v -> ExprBV b v
F.reftPred (RReft -> ReftBV Symbol Symbol
forall b v r. UReftBV b v r -> r
ur_reft RReft
rr)) -> Expr -> Either Expr SpecType
forall a b. a -> Either a b
Left Expr
e
                  Maybe Expr
_ -> SpecType -> Either Expr SpecType
forall a b. b -> Either a b
Right (SpecType -> RReft -> SpecType
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
strengthen SpecType
t' RReft
rr)
              where
                  (SpecType
t', Maybe RReft
ro) = SpecType -> (SpecType, Maybe RReft)
stripRType SpecType
t

stripReft     :: SpecType -> SpecType
stripReft :: SpecType -> SpecType
stripReft SpecType
t   = SpecType -> (RReft -> SpecType) -> Maybe RReft -> SpecType
forall b a. b -> (a -> b) -> Maybe a -> b
maybe SpecType
t' (SpecType -> RReft -> SpecType
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
strengthen SpecType
t') Maybe RReft
ro
  where
    (SpecType
t', Maybe RReft
ro)  = SpecType -> (SpecType, Maybe RReft)
stripRType SpecType
t

stripRType    :: SpecType -> (SpecType, Maybe RReft)
stripRType :: SpecType -> (SpecType, Maybe RReft)
stripRType SpecType
st = (SpecType
forall {v}.
RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol v (ReftBV Symbol Symbol))
t', Maybe RReft
ro)
  where
    t' :: RTypeBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol v (ReftBV Symbol Symbol))
t'        = (RReft -> UReftBV Symbol v (ReftBV Symbol Symbol))
-> SpecType
-> RTypeBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol v (ReftBV Symbol Symbol))
forall a b.
(a -> b)
-> RTypeBV Symbol Symbol RTyCon RTyVar a
-> RTypeBV Symbol Symbol RTyCon RTyVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (UReftBV Symbol v (ReftBV Symbol Symbol)
-> RReft -> UReftBV Symbol v (ReftBV Symbol Symbol)
forall a b. a -> b -> a
const (ReftBV Symbol Symbol -> UReftBV Symbol v (ReftBV Symbol Symbol)
forall r v. r -> UReftV v r
uTop ReftBV Symbol Symbol
forall a. Monoid a => a
mempty)) SpecType
t
    ro :: Maybe RReft
ro        = SpecType -> Maybe RReft
forall b v c tv r. RTypeBV b v c tv r -> Maybe r
stripRTypeBase  SpecType
t
    t :: SpecType
t         = SpecType -> SpecType
simplifyBounds SpecType
st

-- | @sliceREnv xs m@ collects all bindings needed by @xs@.
-- A symbol needs a binding, if the binding binds the symbol, or it contains the
-- symbol, or it contains symbols used by bindings that are needed by the
-- symbol.
sliceREnv :: [F.Symbol] -> Ctx -> [(F.Symbol, SpecType)]
sliceREnv :: [Symbol] -> Ctx -> [(Symbol, SpecType)]
sliceREnv [Symbol]
xs Ctx
m =
    [(Symbol
x, SpecType
t) | Symbol
x <- [Symbol]
relatedSyms, Just SpecType
t <- [Symbol -> Ctx -> Maybe SpecType
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Symbol
x Ctx
m], SpecType -> Bool
forall {t} {t1} {t2}. RTypeBV Symbol Symbol t t1 t2 -> Bool
ok SpecType
t]
  where
    directlyUses :: HashMap Symbol (HashSet Symbol)
directlyUses = (SpecType -> HashSet Symbol)
-> Ctx -> HashMap Symbol (HashSet Symbol)
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map (Expr -> HashSet Symbol
forall v. (Eq v, Hashable v) => ExprBV v v -> HashSet v
F.exprSymbolsSet (Expr -> HashSet Symbol)
-> (SpecType -> Expr) -> SpecType -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReftBV Symbol Symbol -> Expr
forall b v. ReftBV b v -> ExprBV b v
F.reftPred (ReftBV Symbol Symbol -> Expr)
-> (SpecType -> ReftBV Symbol Symbol) -> SpecType -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ReftBV Symbol Symbol
SpecType -> ReftBV (ReftBind RReft) (ReftVar RReft)
forall r b v c tv.
(ToReft r, Binder (ReftBind r)) =>
RTypeBV b v c tv r -> ReftBV (ReftBind r) (ReftVar r)
rTypeReft) Ctx
m
    relatedSyms :: [Symbol]
relatedSyms = [Symbol] -> [Symbol]
forall a. Ord a => [a] -> [a]
L.sort ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
S.toList (HashSet Symbol -> [Symbol]) -> HashSet Symbol -> [Symbol]
forall a b. (a -> b) -> a -> b
$ HashSet Symbol -> HashMap Symbol (HashSet Symbol) -> HashSet Symbol
F.relatedSymbols ([Symbol] -> HashSet Symbol
forall a. Hashable a => [a] -> HashSet a
S.fromList [Symbol]
xs) HashMap Symbol (HashSet Symbol)
directlyUses
    ok :: RTypeBV Symbol Symbol t t1 t2 -> Bool
ok        = Bool -> Bool
not (Bool -> Bool)
-> (RTypeBV Symbol Symbol t t1 t2 -> Bool)
-> RTypeBV Symbol Symbol t t1 t2
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV Symbol Symbol t t1 t2 -> Bool
forall {t} {t1} {t2}. RTypeBV Symbol Symbol t t1 t2 -> Bool
isFunTy

tidyREnvM      :: [F.Symbol] -> CtxM -> [(F.Symbol, WithModel SpecType)]
tidyREnvM :: [Symbol] -> CtxM -> [(Symbol, WithModel SpecType)]
tidyREnvM [Symbol]
xs CtxM
m = [(Symbol
x, WithModel SpecType
t) | Symbol
x <- [Symbol]
xs', WithModel SpecType
t <- Maybe (WithModel SpecType) -> [WithModel SpecType]
forall a. Maybe a -> [a]
maybeToList (Symbol -> CtxM -> Maybe (WithModel SpecType)
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Symbol
x CtxM
m), WithModel SpecType -> Bool
forall {t} {t1} {t2}.
WithModel (RTypeBV Symbol Symbol t t1 t2) -> Bool
ok WithModel SpecType
t]
  where
    xs' :: [Symbol]
xs'       = (Symbol -> [Symbol]) -> [Symbol] -> [Symbol]
forall a. (Eq a, Hashable a) => (a -> [a]) -> [a] -> [a]
expandFix Symbol -> [Symbol]
deps [Symbol]
xs
    deps :: Symbol -> [Variable (ReftBV Symbol Symbol)]
deps Symbol
y    = [Variable (ReftBV Symbol Symbol)]
-> (WithModel SpecType -> [Variable (ReftBV Symbol Symbol)])
-> Maybe (WithModel SpecType)
-> [Variable (ReftBV Symbol Symbol)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (ReftBV Symbol Symbol -> [Variable (ReftBV Symbol Symbol)]
forall a. Subable a => a -> [Variable a]
F.syms (ReftBV Symbol Symbol -> [Variable (ReftBV Symbol Symbol)])
-> (WithModel SpecType -> ReftBV Symbol Symbol)
-> WithModel SpecType
-> [Variable (ReftBV Symbol Symbol)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ReftBV Symbol Symbol
SpecType -> ReftBV (ReftBind RReft) (ReftVar RReft)
forall r b v c tv.
(ToReft r, Binder (ReftBind r)) =>
RTypeBV b v c tv r -> ReftBV (ReftBind r) (ReftVar r)
rTypeReft (SpecType -> ReftBV Symbol Symbol)
-> (WithModel SpecType -> SpecType)
-> WithModel SpecType
-> ReftBV Symbol Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithModel SpecType -> SpecType
forall t. WithModel t -> t
dropModel) (Symbol -> CtxM -> Maybe (WithModel SpecType)
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Symbol
y CtxM
m)
    ok :: WithModel (RTypeBV Symbol Symbol t t1 t2) -> Bool
ok        = Bool -> Bool
not (Bool -> Bool)
-> (WithModel (RTypeBV Symbol Symbol t t1 t2) -> Bool)
-> WithModel (RTypeBV Symbol Symbol t t1 t2)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV Symbol Symbol t t1 t2 -> Bool
forall {t} {t1} {t2}. RTypeBV Symbol Symbol t t1 t2 -> Bool
isFunTy (RTypeBV Symbol Symbol t t1 t2 -> Bool)
-> (WithModel (RTypeBV Symbol Symbol t t1 t2)
    -> RTypeBV Symbol Symbol t t1 t2)
-> WithModel (RTypeBV Symbol Symbol t t1 t2)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithModel (RTypeBV Symbol Symbol t t1 t2)
-> RTypeBV Symbol Symbol t t1 t2
forall t. WithModel t -> t
dropModel

expandFix :: (Eq a, Hashable a) => (a -> [a]) -> [a] -> [a]
expandFix :: forall a. (Eq a, Hashable a) => (a -> [a]) -> [a] -> [a]
expandFix a -> [a]
f               = HashSet a -> [a]
forall a. HashSet a -> [a]
S.toList (HashSet a -> [a]) -> ([a] -> HashSet a) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet a -> [a] -> HashSet a
go HashSet a
forall a. HashSet a
S.empty
  where
    go :: HashSet a -> [a] -> HashSet a
go HashSet a
seen []            = HashSet a
seen
    go HashSet a
seen (a
x:[a]
xs)
      | a
x a -> HashSet a -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
`S.member` HashSet a
seen = HashSet a -> [a] -> HashSet a
go HashSet a
seen [a]
xs
      | Bool
otherwise         = HashSet a -> [a] -> HashSet a
go (a -> HashSet a -> HashSet a
forall a. Hashable a => a -> HashSet a -> HashSet a
S.insert a
x HashSet a
seen) (a -> [a]
f a
x [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
xs)

tidyTemps     :: (F.Subable t, F.Variable t ~ F.Symbol) => [(F.Symbol, t)] -> (F.Subst, [(F.Symbol, t)])
tidyTemps :: forall t.
(Subable t, Variable t ~ Symbol) =>
[(Symbol, t)] -> (SubstV Symbol, [(Symbol, t)])
tidyTemps [(Symbol, t)]
xts = (SubstV Symbol
θ, [(Symbol -> Symbol
txB Symbol
x, t -> t
txTy t
t) | (Symbol
x, t
t) <- [(Symbol, t)]
xts])
  where
    txB :: Symbol -> Symbol
txB  Symbol
x    = Symbol -> Symbol -> HashMap Symbol Symbol -> Symbol
forall k v. Hashable k => v -> k -> HashMap k v -> v
M.lookupDefault Symbol
x Symbol
x HashMap Symbol Symbol
m
    txTy :: t -> t
txTy      = SubstV (Variable t) -> t -> t
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV Symbol
SubstV (Variable t)
θ
    m :: HashMap Symbol Symbol
m         = [(Symbol, Symbol)] -> HashMap Symbol Symbol
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [(Symbol, Symbol)]
yzs
    θ :: SubstV Symbol
θ         = [(Symbol, Expr)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst [(Symbol
y, Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar Symbol
z) | (Symbol
y, Symbol
z) <- [(Symbol, Symbol)]
yzs]
    yzs :: [(Symbol, Symbol)]
yzs       = [Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
ys [Symbol]
niceTemps
    ys :: [Symbol]
ys        = [ Symbol
x | (Symbol
x,t
_) <- [(Symbol, t)]
xts, Symbol -> Bool
GM.isTmpSymbol Symbol
x]

niceTemps     :: [F.Symbol]
niceTemps :: [Symbol]
niceTemps     = [Char] -> Symbol
mkSymbol ([Char] -> Symbol) -> [[Char]] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Char]]
xs [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [[Char]]
ys
  where
    mkSymbol :: [Char] -> Symbol
mkSymbol  = [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Char] -> Symbol) -> ([Char] -> [Char]) -> [Char] -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'?' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
:)
    xs :: [[Char]]
xs        = Char -> [Char]
forall t. t -> [t]
Misc.single (Char -> [Char]) -> [Char] -> [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char
'a' .. Char
'z']
    ys :: [[Char]]
ys        = ([Char]
"a" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([Char] -> [Char]) -> [[Char]] -> [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n | Int
n <- [(Int
0::Int) ..]]