{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleInstances #-}

{-# OPTIONS_GHC -Wno-orphans #-}

---------------------------------------------------------------------
-- | This module contains functions for cleaning up types before
--   they are rendered, e.g. in error messages or annoations,
--   and also some PPrint instances that rely upon tidying.
---------------------------------------------------------------------

module Language.Haskell.Liquid.UX.Tidy (

    -- * Tidying functions
    tidySpecType
  , tidyInternalRefas
  , tidySymbol

    -- * Panic and Exit
  , panicError

    -- * Final result
  , Result (..)

    -- * Error to UserError
  , errorToUserError

    -- * MOVE TO TYPES
  , cinfoError
  ) where

import           Data.Hashable
import           Prelude                                   hiding (error)
import qualified Data.HashMap.Strict                       as M
import qualified Data.HashSet                              as S
import qualified Data.List                                 as L
import qualified Data.Text                                 as T
import qualified Control.Exception                         as Ex
import qualified Language.Haskell.Liquid.GHC.Misc          as GM
-- (dropModuleNames, showPpr, stringTyVar)
import           Language.Fixpoint.Types                   hiding (Result, SrcSpan, Error)
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           Language.Haskell.Liquid.Types.RefType     (rVar, subsTyVarsMeet, FreeVar)
import           Language.Haskell.Liquid.Types.PrettyPrint
import           Data.Generics                             (everywhere, mkT)
import           Text.PrettyPrint.HughesPJ


------------------------------------------------------------------------
-- | Converting Results To Answers -------------------------------------
------------------------------------------------------------------------

class Result a where
  result :: a -> FixResult UserError

instance Result UserError where
  result :: UserError -> FixResult UserError
result UserError
e = [(UserError, Maybe [Char])] -> [Char] -> FixResult UserError
forall a. [(a, Maybe [Char])] -> [Char] -> FixResult a
Crash [(UserError
e, Maybe [Char]
forall a. Maybe a
Nothing)] [Char]
""

instance Result [Error] where
  result :: [Error] -> FixResult UserError
result [Error]
es = [(UserError, Maybe [Char])] -> [Char] -> FixResult UserError
forall a. [(a, Maybe [Char])] -> [Char] -> FixResult a
Crash ([ (Error -> UserError
errorToUserError Error
e, Maybe [Char]
forall a. Maybe a
Nothing) | Error
e <- [Error]
es]) [Char]
""

instance Result Error where
  result :: Error -> FixResult UserError
result Error
e  = [Error] -> FixResult UserError
forall a. Result a => a -> FixResult UserError
result [Error
e] --  Crash [pprint e] ""

instance Result (FixResult Cinfo) where
  result :: FixResult Cinfo -> FixResult UserError
result = (Cinfo -> UserError) -> FixResult Cinfo -> FixResult UserError
forall a b. (a -> b) -> FixResult a -> FixResult b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Error -> UserError
errorToUserError (Error -> UserError) -> (Cinfo -> Error) -> Cinfo -> UserError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cinfo -> Error
cinfoError)

errorToUserError :: Error -> UserError
errorToUserError :: Error -> UserError
errorToUserError = (RTypeV Symbol RTyCon RTyVar RReft -> Doc) -> Error -> UserError
forall a b. (a -> b) -> TError a -> TError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RTypeV Symbol RTyCon RTyVar RReft -> Doc
ppSpecTypeErr

-- TODO: move to Types.hs
cinfoError :: Cinfo -> Error
cinfoError :: Cinfo -> Error
cinfoError (Ci SrcSpan
_ (Just Error
e) Maybe Var
_) = Error
e
cinfoError (Ci SrcSpan
l Maybe Error
_ Maybe Var
_)        = SrcSpan -> Doc -> Error
forall t. SrcSpan -> Doc -> TError t
ErrOther SrcSpan
l ([Char] -> Doc
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Cinfo: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SrcSpan -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr SrcSpan
l)

-------------------------------------------------------------------------
tidySpecType :: Tidy -> SpecType -> SpecType
-------------------------------------------------------------------------
tidySpecType :: Tidy
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidySpecType Tidy
k
  = RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidyEqual
  (RTypeV Symbol RTyCon RTyVar RReft
 -> RTypeV Symbol RTyCon RTyVar RReft)
-> (RTypeV Symbol RTyCon RTyVar RReft
    -> RTypeV Symbol RTyCon RTyVar RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidyValueVars
  (RTypeV Symbol RTyCon RTyVar RReft
 -> RTypeV Symbol RTyCon RTyVar RReft)
-> (RTypeV Symbol RTyCon RTyVar RReft
    -> RTypeV Symbol RTyCon RTyVar RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidyDSymbols
  (RTypeV Symbol RTyCon RTyVar RReft
 -> RTypeV Symbol RTyCon RTyVar RReft)
-> (RTypeV Symbol RTyCon RTyVar RReft
    -> RTypeV Symbol RTyCon RTyVar RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidySymbols Tidy
k
  (RTypeV Symbol RTyCon RTyVar RReft
 -> RTypeV Symbol RTyCon RTyVar RReft)
-> (RTypeV Symbol RTyCon RTyVar RReft
    -> RTypeV Symbol RTyCon RTyVar RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidyInternalRefas
  (RTypeV Symbol RTyCon RTyVar RReft
 -> RTypeV Symbol RTyCon RTyVar RReft)
-> (RTypeV Symbol RTyCon RTyVar RReft
    -> RTypeV Symbol RTyCon RTyVar RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidyLocalRefas Tidy
k
  (RTypeV Symbol RTyCon RTyVar RReft
 -> RTypeV Symbol RTyCon RTyVar RReft)
-> (RTypeV Symbol RTyCon RTyVar RReft
    -> RTypeV Symbol RTyCon RTyVar RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidyFunBinds
  (RTypeV Symbol RTyCon RTyVar RReft
 -> RTypeV Symbol RTyCon RTyVar RReft)
-> (RTypeV Symbol RTyCon RTyVar RReft
    -> RTypeV Symbol RTyCon RTyVar RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidyTyVars

tidyValueVars :: SpecType -> SpecType
tidyValueVars :: RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidyValueVars = (RReft -> RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall r1 r2 v c tv.
(r1 -> r2) -> RTypeV v c tv r1 -> RTypeV v c tv r2
mapReft ((RReft -> RReft)
 -> RTypeV Symbol RTyCon RTyVar RReft
 -> RTypeV Symbol RTyCon RTyVar RReft)
-> (RReft -> RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ \RReft
u -> RReft
u { ur_reft = tidyVV $ ur_reft u }

tidyVV :: Reft -> Reft
tidyVV :: ReftV Symbol -> ReftV Symbol
tidyVV r :: ReftV Symbol
r@(Reft (Symbol
va,Expr
_))
  | Symbol -> Bool
isJunk Symbol
va = ReftV Symbol -> Symbol -> ReftV Symbol
shiftVV ReftV Symbol
r Symbol
v'
  | Bool
otherwise = ReftV Symbol
r
  where
    v' :: Symbol
v'        = if Symbol
v Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol]
xs then Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Text
"v'" :: T.Text) else Symbol
v
    v :: Symbol
v         = Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Text
"v" :: T.Text)
    xs :: [Symbol]
xs        = ReftV Symbol -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms ReftV Symbol
r
    isJunk :: Symbol -> Bool
isJunk    = Symbol -> Symbol -> Bool
isPrefixOfSym Symbol
"x"

tidySymbols :: Tidy -> SpecType -> SpecType
tidySymbols :: Tidy
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidySymbols Tidy
k RTypeV Symbol RTyCon RTyVar RReft
t = (Symbol -> Symbol)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa (Tidy -> Symbol -> Symbol
shortSymbol Tidy
k (Symbol -> Symbol) -> (Symbol -> Symbol) -> Symbol -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
tidySymbol) (RTypeV Symbol RTyCon RTyVar RReft
 -> RTypeV Symbol RTyCon RTyVar RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind Symbol -> Symbol
dropBind RTypeV Symbol RTyCon RTyVar RReft
t
  where
    xs :: HashSet Symbol
xs          = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (RTypeV Symbol RTyCon RTyVar RReft -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms RTypeV Symbol RTyCon RTyVar RReft
t)
    dropBind :: Symbol -> Symbol
dropBind Symbol
x  = if Symbol
x Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
xs then Symbol -> Symbol
tidySymbol Symbol
x else Symbol
nonSymbol

shortSymbol :: Tidy -> Symbol -> Symbol
shortSymbol :: Tidy -> Symbol -> Symbol
shortSymbol Tidy
Lossy = Symbol -> Symbol
GM.dropModuleNames
shortSymbol Tidy
_     = Symbol -> Symbol
forall a. a -> a
id

tidyLocalRefas   :: Tidy -> SpecType -> SpecType
tidyLocalRefas :: Tidy
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidyLocalRefas Tidy
k = (RReft -> RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall r1 r2 v c tv.
(r1 -> r2) -> RTypeV v c tv r1 -> RTypeV v c tv r2
mapReft (Tidy -> RReft -> RReft
forall {v}.
Tidy -> UReftV v (ReftV Symbol) -> UReftV v (ReftV Symbol)
txReft' Tidy
k)
  where
    txReft' :: Tidy -> UReftV v (ReftV Symbol) -> UReftV v (ReftV Symbol)
txReft' Tidy
Full                  = UReftV v (ReftV Symbol) -> UReftV v (ReftV Symbol)
forall a. a -> a
id
    txReft' Tidy
Lossy                 = UReftV v (ReftV Symbol) -> UReftV v (ReftV Symbol)
forall {v}. UReftV v (ReftV Symbol) -> UReftV v (ReftV Symbol)
txReft
    txReft :: UReftV v (ReftV Symbol) -> UReftV v (ReftV Symbol)
txReft UReftV v (ReftV Symbol)
u                      = UReftV v (ReftV Symbol)
u { ur_reft = mapPredReft dropLocals $ ur_reft u }
    dropLocals :: Expr -> Expr
dropLocals                    = ListNE Expr -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd (ListNE Expr -> Expr) -> (Expr -> ListNE Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Bool) -> ListNE Expr -> ListNE Expr
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Symbol -> Bool
isTmp ([Symbol] -> Bool) -> (Expr -> [Symbol]) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms) (ListNE Expr -> ListNE Expr)
-> (Expr -> ListNE Expr) -> Expr -> ListNE Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> ListNE Expr
forall v. Eq v => ExprV v -> [ExprV v]
conjuncts
    isTmp :: Symbol -> Bool
isTmp Symbol
x                       = (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> Symbol -> Bool
`isPrefixOfSym` Symbol
x) [Symbol
anfPrefix, Symbol
"ds_"]

tidyEqual :: SpecType -> SpecType
tidyEqual :: RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidyEqual = (RReft -> RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall r1 r2 v c tv.
(r1 -> r2) -> RTypeV v c tv r1 -> RTypeV v c tv r2
mapReft RReft -> RReft
forall {v}. UReftV v (ReftV Symbol) -> UReftV v (ReftV Symbol)
txReft
  where
    txReft :: UReftV v (ReftV Symbol) -> UReftV v (ReftV Symbol)
txReft UReftV v (ReftV Symbol)
u                      = UReftV v (ReftV Symbol)
u { ur_reft = mapPredReft dropInternals $ ur_reft u }
    dropInternals :: Expr -> Expr
dropInternals                 = ListNE Expr -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd (ListNE Expr -> Expr) -> (Expr -> ListNE Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ListNE Expr -> ListNE Expr
forall a. Eq a => [a] -> [a]
L.nub (ListNE Expr -> ListNE Expr)
-> (Expr -> ListNE Expr) -> Expr -> ListNE Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> ListNE Expr
forall v. Eq v => ExprV v -> [ExprV v]
conjuncts

-- | Drop conjuncts that contain data constructor testing or
-- selector functions.
tidyInternalRefas   :: SpecType -> SpecType
tidyInternalRefas :: RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidyInternalRefas = (RReft -> RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall r1 r2 v c tv.
(r1 -> r2) -> RTypeV v c tv r1 -> RTypeV v c tv r2
mapReft RReft -> RReft
forall {v}. UReftV v (ReftV Symbol) -> UReftV v (ReftV Symbol)
txReft
  where
    txReft :: UReftV v (ReftV Symbol) -> UReftV v (ReftV Symbol)
txReft UReftV v (ReftV Symbol)
u                      = UReftV v (ReftV Symbol)
u { ur_reft = mapPredReft dropInternals $ ur_reft u }
    dropInternals :: Expr -> Expr
dropInternals                 = ListNE Expr -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd (ListNE Expr -> Expr) -> (Expr -> ListNE Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Bool) -> ListNE Expr -> ListNE Expr
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Symbol -> Bool
isIntern ([Symbol] -> Bool) -> (Expr -> [Symbol]) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms) (ListNE Expr -> ListNE Expr)
-> (Expr -> ListNE Expr) -> Expr -> ListNE Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> ListNE Expr
forall v. Eq v => ExprV v -> [ExprV v]
conjuncts
    isIntern :: Symbol -> Bool
isIntern Symbol
x                    = Symbol
"is$" Symbol -> Symbol -> Bool
`isPrefixOfSym` Symbol
x Bool -> Bool -> Bool
|| Symbol
"$select" Symbol -> Symbol -> Bool
`isSuffixOfSym` Symbol
x


tidyDSymbols :: SpecType -> SpecType
tidyDSymbols :: RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidyDSymbols RTypeV Symbol RTyCon RTyVar RReft
t = (Symbol -> Symbol)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind Symbol -> Symbol
tx (RTypeV Symbol RTyCon RTyVar RReft
 -> RTypeV Symbol RTyCon RTyVar RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
tx RTypeV Symbol RTyCon RTyVar RReft
t
  where
    tx :: Symbol -> Symbol
tx         = [Symbol] -> Symbol -> Symbol
bindersTx [Symbol
x | Symbol
x <- RTypeV Symbol RTyCon RTyVar RReft -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms RTypeV Symbol RTyCon RTyVar RReft
t, Symbol -> Bool
isTmp Symbol
x]
    isTmp :: Symbol -> Bool
isTmp      = (Symbol
tempPrefix Symbol -> Symbol -> Bool
`isPrefixOfSym`)

tidyFunBinds :: SpecType -> SpecType
tidyFunBinds :: RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidyFunBinds RTypeV Symbol RTyCon RTyVar RReft
t = (Symbol -> Symbol)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind Symbol -> Symbol
tx (RTypeV Symbol RTyCon RTyVar RReft
 -> RTypeV Symbol RTyCon RTyVar RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
tx RTypeV Symbol RTyCon RTyVar RReft
t
  where
    tx :: Symbol -> Symbol
tx         = [Symbol] -> Symbol -> Symbol
bindersTx ([Symbol] -> Symbol -> Symbol) -> [Symbol] -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ (Symbol -> Bool) -> [Symbol] -> [Symbol]
forall a. (a -> Bool) -> [a] -> [a]
filter Symbol -> Bool
GM.isTmpSymbol ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ RTypeV Symbol RTyCon RTyVar RReft -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeV Symbol RTyCon RTyVar RReft
t

tidyTyVars :: SpecType -> SpecType
tidyTyVars :: RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidyTyVars RTypeV Symbol RTyCon RTyVar RReft
t = [(RTyVar, RType RTyCon RTyVar (),
  RTypeV Symbol RTyCon RTyVar RReft)]
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall k r c.
(Eq k, Hashable k, Reftable r, TyConable c,
 SubsTy k (RType c k ()) c, SubsTy k (RType c k ()) r,
 SubsTy k (RType c k ()) k, SubsTy k (RType c k ()) (RType c k ()),
 SubsTy k (RType c k ()) (RTVar k (RType c k ())), FreeVar c k) =>
[(k, RType c k (), RType c k r)] -> RType c k r -> RType c k r
subsTyVarsAll [(RTyVar, RType RTyCon RTyVar (),
  RTypeV Symbol RTyCon RTyVar RReft)]
forall {c}.
[(RTyVar, RTypeV Symbol c RTyVar (), RTypeV Symbol c RTyVar RReft)]
αβs RTypeV Symbol RTyCon RTyVar RReft
t
  where
    αβs :: [(RTyVar, RTypeV Symbol c RTyVar (), RTypeV Symbol c RTyVar RReft)]
αβs  = (RTyVar
 -> RTypeV Symbol c RTyVar RReft
 -> (RTyVar, RTypeV Symbol c RTyVar (),
     RTypeV Symbol c RTyVar RReft))
-> [RTyVar]
-> [RTypeV Symbol c RTyVar RReft]
-> [(RTyVar, RTypeV Symbol c RTyVar (),
     RTypeV Symbol c RTyVar RReft)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\RTyVar
α RTypeV Symbol c RTyVar RReft
β -> (RTyVar
α, RTypeV Symbol c RTyVar RReft -> RTypeV Symbol c RTyVar ()
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv ()
toRSort RTypeV Symbol c RTyVar RReft
β, RTypeV Symbol c RTyVar RReft
β)) [RTyVar]
αs [RTypeV Symbol c RTyVar RReft]
forall {c}. [RType c RTyVar RReft]
βs
    αs :: [RTyVar]
αs   = [RTyVar] -> [RTyVar]
forall a. Eq a => [a] -> [a]
L.nub (RTypeV Symbol RTyCon RTyVar RReft -> [RTyVar]
forall c tv r. RType c tv r -> [tv]
tyVars RTypeV Symbol RTyCon RTyVar RReft
t)
    βs :: [RType c RTyVar RReft]
βs   = ([Char] -> RType c RTyVar RReft)
-> [[Char]] -> [RType c RTyVar RReft]
forall a b. (a -> b) -> [a] -> [b]
map (Var -> RType c RTyVar RReft
forall r c. Monoid r => Var -> RType c RTyVar r
rVar (Var -> RType c RTyVar RReft)
-> ([Char] -> Var) -> [Char] -> RType c RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Var
GM.stringTyVar) [[Char]]
pool
    pool :: [[Char]]
pool = [[Char
c] | Char
c <- [Char
'a'..Char
'z']] [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [ [Char]
"t" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i | Int
i <- [(Int
1::Int)..]]


bindersTx :: [Symbol] -> Symbol -> Symbol
bindersTx :: [Symbol] -> Symbol -> Symbol
bindersTx [Symbol]
ds   = \Symbol
y -> Symbol -> Symbol -> HashMap Symbol Symbol -> Symbol
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Symbol
y Symbol
y HashMap Symbol Symbol
m
  where
    m :: HashMap Symbol Symbol
m          = [(Symbol, Symbol)] -> HashMap Symbol Symbol
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Symbol, Symbol)] -> HashMap Symbol Symbol)
-> [(Symbol, Symbol)] -> HashMap Symbol Symbol
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
ds ([Symbol] -> [(Symbol, Symbol)]) -> [Symbol] -> [(Symbol, Symbol)]
forall a b. (a -> b) -> a -> b
$ Int -> Symbol
var (Int -> Symbol) -> [Int] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int
1::Int)..]
    var :: Int -> Symbol
var        = [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol ([Char] -> Symbol) -> (Int -> [Char]) -> Int -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'x' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
:) ([Char] -> [Char]) -> (Int -> [Char]) -> Int -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char]
forall a. Show a => a -> [Char]
show


tyVars :: RType c tv r -> [tv]
tyVars :: forall c tv r. RType c tv r -> [tv]
tyVars (RAllP PVUV Symbol c tv
_ RTypeV Symbol c tv r
t)       = RTypeV Symbol c tv r -> [tv]
forall c tv r. RType c tv r -> [tv]
tyVars RTypeV Symbol c tv r
t
tyVars (RAllT RTVUV Symbol c tv
α RTypeV Symbol c tv r
t r
_)     = RTVUV Symbol c tv -> tv
forall tv s. RTVar tv s -> tv
ty_var_value RTVUV Symbol c tv
α tv -> [tv] -> [tv]
forall a. a -> [a] -> [a]
: RTypeV Symbol c tv r -> [tv]
forall c tv r. RType c tv r -> [tv]
tyVars RTypeV Symbol c tv r
t
tyVars (RFun Symbol
_ RFInfo
_ RTypeV Symbol c tv r
t RTypeV Symbol c tv r
t' r
_) = RTypeV Symbol c tv r -> [tv]
forall c tv r. RType c tv r -> [tv]
tyVars RTypeV Symbol c tv r
t [tv] -> [tv] -> [tv]
forall a. [a] -> [a] -> [a]
++ RTypeV Symbol c tv r -> [tv]
forall c tv r. RType c tv r -> [tv]
tyVars RTypeV Symbol c tv r
t'
tyVars (RAppTy RTypeV Symbol c tv r
t RTypeV Symbol c tv r
t' r
_)   = RTypeV Symbol c tv r -> [tv]
forall c tv r. RType c tv r -> [tv]
tyVars RTypeV Symbol c tv r
t [tv] -> [tv] -> [tv]
forall a. [a] -> [a] -> [a]
++ RTypeV Symbol c tv r -> [tv]
forall c tv r. RType c tv r -> [tv]
tyVars RTypeV Symbol c tv r
t'
tyVars (RApp c
_ [RTypeV Symbol c tv r]
ts [RTPropV Symbol c tv r]
_ r
_)   = (RTypeV Symbol c tv r -> [tv]) -> [RTypeV Symbol c tv r] -> [tv]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RTypeV Symbol c tv r -> [tv]
forall c tv r. RType c tv r -> [tv]
tyVars [RTypeV Symbol c tv r]
ts
tyVars (RVar tv
α r
_)        = [tv
α]
tyVars (RAllE Symbol
_ RTypeV Symbol c tv r
_ RTypeV Symbol c tv r
t)     = RTypeV Symbol c tv r -> [tv]
forall c tv r. RType c tv r -> [tv]
tyVars RTypeV Symbol c tv r
t
tyVars (REx Symbol
_ RTypeV Symbol c tv r
_ RTypeV Symbol c tv r
t)       = RTypeV Symbol c tv r -> [tv]
forall c tv r. RType c tv r -> [tv]
tyVars RTypeV Symbol c tv r
t
tyVars (RExprArg Located Expr
_)      = []
tyVars (RRTy [(Symbol, RTypeV Symbol c tv r)]
_ r
_ Oblig
_ RTypeV Symbol c tv r
t)    = RTypeV Symbol c tv r -> [tv]
forall c tv r. RType c tv r -> [tv]
tyVars RTypeV Symbol c tv r
t
tyVars (RHole r
_)         = []

subsTyVarsAll
  :: (Eq k, Hashable k,
      Reftable r, TyConable c, SubsTy k (RType c k ()) c,
      SubsTy k (RType c k ()) r,
      SubsTy k (RType c k ()) k,
      SubsTy k (RType c k ()) (RType c k ()),
      SubsTy k (RType c k ()) (RTVar k (RType c k ())),
      FreeVar c k)
   => [(k, RType c k (), RType c k r)] -> RType c k r -> RType c k r
subsTyVarsAll :: forall k r c.
(Eq k, Hashable k, Reftable r, TyConable c,
 SubsTy k (RType c k ()) c, SubsTy k (RType c k ()) r,
 SubsTy k (RType c k ()) k, SubsTy k (RType c k ()) (RType c k ()),
 SubsTy k (RType c k ()) (RTVar k (RType c k ())), FreeVar c k) =>
[(k, RType c k (), RType c k r)] -> RType c k r -> RType c k r
subsTyVarsAll [(k, RType c k (), RType c k r)]
ats = RType c k r -> RType c k r
go
  where
    abm :: HashMap k k
abm            = [(k, k)] -> HashMap k k
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(k
a, k
b) | (k
a, RType c k ()
_, RVar k
b r
_) <- [(k, RType c k (), RType c k r)]
ats]
    go :: RType c k r -> RType c k r
go (RAllT RTVar k (RType c k ())
a RType c k r
t r
r) = RTVar k (RType c k ()) -> RType c k r -> r -> RType c k r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT (k -> RTVar k (RType c k ())
forall tv s. tv -> RTVar tv s
makeRTVar (k -> RTVar k (RType c k ())) -> k -> RTVar k (RType c k ())
forall a b. (a -> b) -> a -> b
$ k -> k -> HashMap k k -> k
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault (RTVar k (RType c k ()) -> k
forall tv s. RTVar tv s -> tv
ty_var_value RTVar k (RType c k ())
a) (RTVar k (RType c k ()) -> k
forall tv s. RTVar tv s -> tv
ty_var_value RTVar k (RType c k ())
a) HashMap k k
abm) (RType c k r -> RType c k r
go RType c k r
t) r
r
    go RType c k r
t           = [(k, RType c k (), RType c k r)] -> RType c k r -> RType c k r
forall tv (t :: * -> *) r c.
(Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarsMeet [(k, RType c k (), RType c k r)]
ats RType c k r
t


funBinds :: RType t t1 t2 -> [Symbol]
funBinds :: forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds (RAllT RTVUV Symbol t t1
_ RTypeV Symbol t t1 t2
t t2
_)      = RTypeV Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeV Symbol t t1 t2
t
funBinds (RAllP PVUV Symbol t t1
_ RTypeV Symbol t t1 t2
t)        = RTypeV Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeV Symbol t t1 t2
t
funBinds (RFun Symbol
b RFInfo
_ RTypeV Symbol t t1 t2
t1 RTypeV Symbol t t1 t2
t2 t2
_) = Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: RTypeV Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeV Symbol t t1 t2
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RTypeV Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeV Symbol t t1 t2
t2
funBinds (RApp t
_ [RTypeV Symbol t t1 t2]
ts [RTPropV Symbol t t1 t2]
_ t2
_)    = (RTypeV Symbol t t1 t2 -> [Symbol])
-> [RTypeV Symbol t t1 t2] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RTypeV Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds [RTypeV Symbol t t1 t2]
ts
funBinds (RAllE Symbol
b RTypeV Symbol t t1 t2
t1 RTypeV Symbol t t1 t2
t2)    = Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: RTypeV Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeV Symbol t t1 t2
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RTypeV Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeV Symbol t t1 t2
t2
funBinds (REx Symbol
b RTypeV Symbol t t1 t2
t1 RTypeV Symbol t t1 t2
t2)      = Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: RTypeV Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeV Symbol t t1 t2
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RTypeV Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeV Symbol t t1 t2
t2
funBinds (RVar t1
_ t2
_)         = []
funBinds (RRTy [(Symbol, RTypeV Symbol t t1 t2)]
_ t2
_ Oblig
_ RTypeV Symbol t t1 t2
t)     = RTypeV Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeV Symbol t t1 t2
t
funBinds (RAppTy RTypeV Symbol t t1 t2
t1 RTypeV Symbol t t1 t2
t2 t2
_)   = RTypeV Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeV Symbol t t1 t2
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RTypeV Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeV Symbol t t1 t2
t2
funBinds (RExprArg Located Expr
_)       = []
funBinds (RHole t2
_)          = []


--------------------------------------------------------------------------------
-- | Show an Error, then crash
--------------------------------------------------------------------------------
panicError :: {-(?callStack :: CallStack) =>-} Error -> a
--------------------------------------------------------------------------------
panicError :: forall a. Error -> a
panicError = Error -> a
forall a e. (?callStack::CallStack, Exception e) => e -> a
Ex.throw

-- ^ This function is put in this module as it depends on the Exception instance,
--   which depends on the PPrint instance, which depends on tidySpecType.

--------------------------------------------------------------------------------
-- | Pretty Printing Error Messages --------------------------------------------
--------------------------------------------------------------------------------

-- | Need to put @PPrint Error@ instance here (instead of in Types),
--   as it depends on @PPrint SpecTypes@, which lives in this module.


instance PPrint (CtxError Doc) where
  pprintTidy :: Tidy -> CtxError Doc -> Doc
pprintTidy Tidy
k CtxError Doc
ce = Tidy -> Doc -> UserError -> Doc
forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError Tidy
k (CtxError Doc -> Doc
forall t. CtxError t -> Doc
ctCtx CtxError Doc
ce) (UserError -> Doc) -> UserError -> Doc
forall a b. (a -> b) -> a -> b
$ CtxError Doc -> UserError
forall t. CtxError t -> TError t
ctErr CtxError Doc
ce

instance PPrint (CtxError SpecType) where
  pprintTidy :: Tidy -> CtxError (RTypeV Symbol RTyCon RTyVar RReft) -> Doc
pprintTidy Tidy
k CtxError (RTypeV Symbol RTyCon RTyVar RReft)
ce = Tidy -> Doc -> UserError -> Doc
forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError Tidy
k (CtxError (RTypeV Symbol RTyCon RTyVar RReft) -> Doc
forall t. CtxError t -> Doc
ctCtx CtxError (RTypeV Symbol RTyCon RTyVar RReft)
ce) (UserError -> Doc) -> UserError -> Doc
forall a b. (a -> b) -> a -> b
$ RTypeV Symbol RTyCon RTyVar RReft -> Doc
ppSpecTypeErr (RTypeV Symbol RTyCon RTyVar RReft -> Doc) -> Error -> UserError
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtxError (RTypeV Symbol RTyCon RTyVar RReft) -> Error
forall t. CtxError t -> TError t
ctErr CtxError (RTypeV Symbol RTyCon RTyVar RReft)
ce

instance PPrint Error where
  pprintTidy :: Tidy -> Error -> Doc
pprintTidy Tidy
k = Tidy -> Doc -> UserError -> Doc
forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError Tidy
k Doc
empty (UserError -> Doc) -> (Error -> UserError) -> Error -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RTypeV Symbol RTyCon RTyVar RReft -> Doc) -> Error -> UserError
forall a b. (a -> b) -> TError a -> TError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RTypeV Symbol RTyCon RTyVar RReft -> Doc
ppSpecTypeErr

ppSpecTypeErr :: SpecType -> Doc
ppSpecTypeErr :: RTypeV Symbol RTyCon RTyVar RReft -> Doc
ppSpecTypeErr = Tidy -> RTypeV Symbol RTyCon RTyVar RReft -> Doc
ppSpecType Tidy
Lossy

ppSpecType :: Tidy -> SpecType -> Doc
ppSpecType :: Tidy -> RTypeV Symbol RTyCon RTyVar RReft -> Doc
ppSpecType Tidy
k = Tidy -> RTypeV Symbol RTyCon RTyVar RReft -> Doc
forall c tv r. OkRT c tv r => Tidy -> RType c tv r -> Doc
rtypeDoc     Tidy
k
             (RTypeV Symbol RTyCon RTyVar RReft -> Doc)
-> (RTypeV Symbol RTyCon RTyVar RReft
    -> RTypeV Symbol RTyCon RTyVar RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
tidySpecType Tidy
k
             (RTypeV Symbol RTyCon RTyVar RReft
 -> RTypeV Symbol RTyCon RTyVar RReft)
-> (RTypeV Symbol RTyCon RTyVar RReft
    -> RTypeV Symbol RTyCon RTyVar RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RReft -> RReft)
-> RTypeV Symbol RTyCon RTyVar RReft
-> RTypeV Symbol RTyCon RTyVar RReft
forall a b.
(a -> b)
-> RTypeV Symbol RTyCon RTyVar a -> RTypeV Symbol RTyCon RTyVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere ((Expr -> Expr) -> a -> a
forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT Expr -> Expr
noCasts))
  where
    noCasts :: Expr -> Expr
    noCasts :: Expr -> Expr
noCasts (ECst Expr
x Sort
_) = Expr
x
    noCasts Expr
e          = Expr
e

instance Show Error where
  show :: Error -> [Char]
show Error
e = Doc -> [Char]
render (SrcSpan -> Doc
forall a. PPrint a => a -> Doc
pprint (Error -> SrcSpan
forall t. TError t -> SrcSpan
pos Error
e) Doc -> Doc -> Doc
<+> Error -> Doc
forall a. PPrint a => a -> Doc
pprint Error
e)

instance Ex.Exception Error
instance Ex.Exception [Error]