{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections     #-}
{-# 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 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           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Transforms.Simplify
import           Language.Haskell.Liquid.UX.Tidy
import           Language.Haskell.Liquid.Types
import qualified Language.Haskell.Liquid.GHC.Misc    as GM
import qualified Language.Haskell.Liquid.Misc        as Misc
import qualified Language.Fixpoint.Misc              as Misc

-- import Debug.Trace

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

------------------------------------------------------------------------
tidyError :: Config -> F.FixSolution -> Error -> Error
------------------------------------------------------------------------
tidyError :: Config -> FixSolution -> Error -> Error
tidyError Config
cfg FixSolution
sol
  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Tidy -> SpecType -> SpecType
tidySpecType Tidy
tidy)
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy -> FixSolution -> Error -> Error
tidyErrContext Tidy
tidy FixSolution
sol
  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 -> F.FixSolution -> Error -> Error
tidyErrContext :: Tidy -> FixSolution -> Error -> Error
tidyErrContext Tidy
k FixSolution
_ e :: Error
e@(ErrSubType {})
  = Error
e { ctx :: HashMap Symbol SpecType
ctx = HashMap Symbol SpecType
c', tact :: SpecType
tact = forall a. Subable a => Subst -> a -> a
F.subst Subst
θ SpecType
tA, texp :: SpecType
texp = forall a. Subable a => Subst -> a -> a
F.subst Subst
θ SpecType
tE }
    where
      (Subst
θ, HashMap Symbol SpecType
c') = Tidy
-> [Symbol]
-> HashMap Symbol SpecType
-> (Subst, HashMap Symbol SpecType)
tidyCtx Tidy
k [Symbol]
xs (forall t. TError t -> HashMap Symbol t
ctx Error
e)
      xs :: [Symbol]
xs      = forall a. Subable a => a -> [Symbol]
F.syms SpecType
tA forall a. [a] -> [a] -> [a]
++ forall a. Subable a => a -> [Symbol]
F.syms SpecType
tE
      tA :: SpecType
tA      = forall t. TError t -> t
tact Error
e
      tE :: SpecType
tE      = forall t. TError t -> t
texp Error
e

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

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

tidyErrContext Tidy
_ FixSolution
_ Error
e
  = Error
e

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

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

tidyREnv :: [(F.Symbol, SpecType)] -> (F.Subst, [(F.Symbol, SpecType)])
tidyREnv :: [(Symbol, SpecType)] -> (Subst, [(Symbol, SpecType)])
tidyREnv [(Symbol, SpecType)]
xts    = (Subst
θ, forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (forall a. Subable a => Subst -> a -> a
F.subst Subst
θ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SpecType)]
zts)
  where
    θ :: Subst
θ           = [(Symbol, Expr)] -> Subst
expandVarDefs [(Symbol, Expr)]
yes
    ([(Symbol, Expr)]
yes, [(Symbol, SpecType)]
zts)  = forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
Misc.mapEither 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)] -> Subst
expandVarDefs      = Subst -> [(Symbol, Expr)] -> Subst
go forall a. Monoid a => a
mempty
  where
    go :: Subst -> [(Symbol, Expr)] -> Subst
go !Subst
su [(Symbol, Expr)]
xes
      | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Symbol, Expr)]
yes   = Subst
su forall a. Monoid a => a -> a -> a
`mappend` [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol, Expr)]
xes
      | Bool
otherwise  = Subst -> [(Symbol, Expr)] -> Subst
go (Subst
su forall a. Monoid a => a -> a -> a
`mappend` Subst
su') [(Symbol, Expr)]
xes''
      where
       xes'' :: [(Symbol, Expr)]
xes''       = [(Symbol
z, forall a. Subable a => Subst -> a -> a
F.subst Subst
su' Expr
e) | (Symbol
z, Expr
e) <- [(Symbol, Expr)]
zes]
       xs :: HashSet Symbol
xs          = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Symbol
x | (Symbol
x, Expr
_) <- [(Symbol, Expr)]
xes]
       su' :: Subst
su'         = [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol, Expr)]
yes
       ([(Symbol, Expr)]
yes, [(Symbol, Expr)]
zes)  = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (forall {a}. Subable a => HashSet Symbol -> a -> Bool
isDef HashSet Symbol
xs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Symbol, Expr)]
xes
    isDef :: HashSet Symbol -> a -> Bool
isDef HashSet Symbol
xs a
e     = Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
xs) (forall a. Subable a => a -> [Symbol]
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) = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
x,)) (forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
x,)) (SpecType -> Either Expr SpecType
isInline' SpecType
t)

isInline' :: SpecType -> Either F.Expr SpecType
isInline' :: SpecType -> Either Expr SpecType
isInline' SpecType
t = case Maybe RReft
ro of
                Maybe RReft
Nothing -> forall a b. b -> Either a b
Right SpecType
t'
                Just RReft
rr -> case Reft -> Maybe Expr
F.isSingletonReft (forall r. UReft r -> r
ur_reft RReft
rr) of
                             Just Expr
e  -> forall a b. a -> Either a b
Left Expr
e
                             Maybe Expr
Nothing -> forall a b. b -> Either a b
Right (forall r c tv. Reftable r => RType c tv r -> r -> RType 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   = forall b a. b -> (a -> b) -> Maybe a -> b
maybe SpecType
t' (forall r c tv. Reftable r => RType c tv r -> r -> RType 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
t', Maybe RReft
ro)
  where
    t' :: SpecType
t'        = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. a -> b -> a
const (forall r. r -> UReft r
uTop forall a. Monoid a => a
mempty)) SpecType
t
    ro :: Maybe RReft
ro        = forall c tv r. RType c tv r -> Maybe r
stripRTypeBase  SpecType
t
    t :: SpecType
t         = SpecType -> SpecType
simplifyBounds SpecType
st

sliceREnv :: [F.Symbol] -> Ctx -> [(F.Symbol, SpecType)]
sliceREnv :: [Symbol] -> HashMap Symbol SpecType -> [(Symbol, SpecType)]
sliceREnv [Symbol]
xs HashMap Symbol SpecType
m = [(Symbol
x, SpecType
t) | Symbol
x <- [Symbol]
xs', SpecType
t <- forall a. Maybe a -> [a]
maybeToList (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
x HashMap Symbol SpecType
m), forall {t} {t1} {t2}. RType t t1 t2 -> Bool
ok SpecType
t]
  where
    xs' :: [Symbol]
xs'       = forall a. (Eq a, Hashable a) => (a -> [a]) -> [a] -> [a]
expandFix Symbol -> [Symbol]
deps [Symbol]
xs
    deps :: Symbol -> [Symbol]
deps Symbol
y    = forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (forall a. Subable a => a -> [Symbol]
F.syms forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r c tv. Reftable r => RType c tv r -> Reft
rTypeReft) (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
y HashMap Symbol SpecType
m)
    ok :: RType t t1 t2 -> Bool
ok        = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {t} {t1} {t2}. RType t t1 t2 -> Bool
isFunTy

tidyREnvM      :: [F.Symbol] -> CtxM -> [(F.Symbol, WithModel SpecType)]
tidyREnvM :: [Symbol]
-> HashMap Symbol (WithModel SpecType)
-> [(Symbol, WithModel SpecType)]
tidyREnvM [Symbol]
xs HashMap Symbol (WithModel SpecType)
m = [(Symbol
x, WithModel SpecType
t) | Symbol
x <- [Symbol]
xs', WithModel SpecType
t <- forall a. Maybe a -> [a]
maybeToList (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
x HashMap Symbol (WithModel SpecType)
m), forall {t} {t1} {t2}. WithModel (RType t t1 t2) -> Bool
ok WithModel SpecType
t]
  where
    xs' :: [Symbol]
xs'       = forall a. (Eq a, Hashable a) => (a -> [a]) -> [a] -> [a]
expandFix Symbol -> [Symbol]
deps [Symbol]
xs
    deps :: Symbol -> [Symbol]
deps Symbol
y    = forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (forall a. Subable a => a -> [Symbol]
F.syms forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r c tv. Reftable r => RType c tv r -> Reft
rTypeReft forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. WithModel t -> t
dropModel) (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
y HashMap Symbol (WithModel SpecType)
m)
    ok :: WithModel (RType t t1 t2) -> Bool
ok        = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {t} {t1} {t2}. RType t t1 t2 -> Bool
isFunTy forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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               = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet a -> [a] -> HashSet a
go 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 forall a. (Eq 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 (forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert a
x HashSet a
seen) (a -> [a]
f a
x forall a. [a] -> [a] -> [a]
++ [a]
xs)

tidyTemps     :: (F.Subable t) => [(F.Symbol, t)] -> (F.Subst, [(F.Symbol, t)])
tidyTemps :: forall t. Subable t => [(Symbol, t)] -> (Subst, [(Symbol, t)])
tidyTemps [(Symbol, t)]
xts = (Subst
θ, [(Symbol -> Symbol
txB Symbol
x, t -> t
txTy t
t) | (Symbol
x, t
t) <- [(Symbol, t)]
xts])
  where
    txB :: Symbol -> Symbol
txB  Symbol
x    = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Symbol
x Symbol
x HashMap Symbol Symbol
m
    txTy :: t -> t
txTy      = forall a. Subable a => Subst -> a -> a
F.subst Subst
θ
    m :: HashMap Symbol Symbol
m         = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Symbol, Symbol)]
yzs
    θ :: Subst
θ         = [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
y, Symbol -> Expr
F.EVar Symbol
z) | (Symbol
y, Symbol
z) <- [(Symbol, Symbol)]
yzs]
    yzs :: [(Symbol, Symbol)]
yzs       = 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Char]]
xs forall a. [a] -> [a] -> [a]
++ [[Char]]
ys
  where
    mkSymbol :: [Char] -> Symbol
mkSymbol  = forall a. Symbolic a => a -> Symbol
F.symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'?' forall a. a -> [a] -> [a]
:)
    xs :: [[Char]]
xs        = forall t. t -> [t]
Misc.single forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char
'a' .. Char
'z']
    ys :: [[Char]]
ys        = ([Char]
"a" forall a. [a] -> [a] -> [a]
++) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [forall a. Show a => a -> [Char]
show Int
n | Int
n <- [(Int
0::Int) ..]]