{-# 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
  = (SpecType -> SpecType) -> Error -> Error
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 -> 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 = Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst Subst
θ SpecType
tA, texp :: SpecType
texp = Subst -> SpecType -> SpecType
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 (Error -> HashMap Symbol SpecType
forall t. TError t -> HashMap Symbol t
ctx Error
e)
      xs :: [Symbol]
xs      = SpecType -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms SpecType
tA [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Symbol]
forall a. Subable a => a -> [Symbol]
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
_ FixSolution
_ e :: Error
e@(ErrSubTypeModel {})
  = Error
e { ctxM :: HashMap Symbol (WithModel SpecType)
ctxM = HashMap Symbol (WithModel SpecType)
c', tactM :: WithModel SpecType
tactM = (SpecType -> SpecType) -> WithModel SpecType -> WithModel SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst Subst
θ) WithModel SpecType
tA, texp :: SpecType
texp = (RReft -> RReft) -> SpecType -> SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst -> RReft -> RReft
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 (HashMap Symbol (WithModel SpecType)
 -> (Subst, HashMap Symbol (WithModel SpecType)))
-> HashMap Symbol (WithModel SpecType)
-> (Subst, HashMap Symbol (WithModel SpecType))
forall a b. (a -> b) -> a -> b
$ Error -> HashMap Symbol (WithModel SpecType)
forall t. TError t -> HashMap Symbol (WithModel t)
ctxM Error
e
      xs :: [Symbol]
xs      = WithModel SpecType -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms WithModel SpecType
tA [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Symbol]
forall a. Subable a => a -> [Symbol]
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 FixSolution
_ e :: Error
e@(ErrAssType {})
  = Error
e { ctx :: HashMap Symbol SpecType
ctx = HashMap Symbol SpecType
c', cond :: SpecType
cond = Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst Subst
θ SpecType
p }
    where
      m :: HashMap Symbol SpecType
m       = Error -> HashMap Symbol SpecType
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      = SpecType -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms SpecType
p
      p :: SpecType
p       = Error -> SpecType
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 Subst -> Subst -> Subst
forall a. Monoid a => a -> a -> a
`mappend` Subst
θ2, [(Symbol, SpecType)] -> HashMap Symbol SpecType
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Symbol, SpecType)]
yts)
  where
    yts :: [(Symbol, SpecType)]
yts        = [Symbol -> SpecType -> (Symbol, SpecType)
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) = [(Symbol, SpecType)] -> (Subst, [(Symbol, SpecType)])
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', RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
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
θ, [(Symbol, WithModel SpecType)]
-> HashMap Symbol (WithModel SpecType)
forall k v. (Eq k, 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 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)  = [(Symbol, WithModel SpecType)]
-> (Subst, [(Symbol, WithModel SpecType)])
forall t. Subable t => [(Symbol, t)] -> (Subst, [(Symbol, t)])
tidyTemps ([(Symbol, WithModel SpecType)]
 -> (Subst, [(Symbol, WithModel SpecType)]))
-> [(Symbol, WithModel SpecType)]
-> (Subst, [(Symbol, WithModel SpecType)])
forall a b. (a -> b) -> a -> b
$ (WithModel SpecType -> WithModel SpecType)
-> (Symbol, WithModel SpecType) -> (Symbol, WithModel SpecType)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((SpecType -> SpecType) -> WithModel SpecType -> WithModel SpecType
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]
-> 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', (RType c tv (f Reft) -> RType c tv (f Reft))
-> f (RType c tv (f Reft)) -> f (RType c tv (f Reft))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\RType c tv (f Reft)
t -> RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
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') 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
θ, (SpecType -> SpecType) -> (Symbol, SpecType) -> (Symbol, SpecType)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst Subst
θ) ((Symbol, SpecType) -> (Symbol, SpecType))
-> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
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)  = ((Symbol, SpecType) -> Either (Symbol, Expr) (Symbol, SpecType))
-> [(Symbol, SpecType)] -> ([(Symbol, Expr)], [(Symbol, SpecType)])
forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
Misc.mapEither (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)] -> Subst
expandVarDefs      = Subst -> [(Symbol, Expr)] -> Subst
go Subst
forall a. Monoid a => a
mempty 
  where 
    go :: Subst -> [(Symbol, Expr)] -> Subst
go !Subst
su [(Symbol, Expr)]
xes     
      | [(Symbol, Expr)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Symbol, Expr)]
yes   = Subst
su Subst -> Subst -> Subst
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 Subst -> Subst -> Subst
forall a. Monoid a => a -> a -> a
`mappend` Subst
su') [(Symbol, Expr)]
xes''
      where  
       xes'' :: [(Symbol, Expr)]
xes''       = [(Symbol
z, Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
F.subst Subst
su' Expr
e) | (Symbol
z, Expr
e) <- [(Symbol, Expr)]
zes] 
       xs :: HashSet Symbol
xs          = [Symbol] -> HashSet Symbol
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)  = ((Symbol, Expr) -> Bool)
-> [(Symbol, Expr)] -> ([(Symbol, Expr)], [(Symbol, Expr)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (HashSet Symbol -> Expr -> Bool
forall a. Subable a => HashSet Symbol -> a -> Bool
isDef HashSet Symbol
xs (Expr -> Bool)
-> ((Symbol, Expr) -> Expr) -> (Symbol, Expr) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Expr) -> Expr
forall a b. (a, b) -> b
snd) [(Symbol, Expr)]
xes 
    isDef :: HashSet Symbol -> a -> Bool
isDef HashSet Symbol
xs a
e     = (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (Symbol -> Bool) -> Symbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
xs)) (a -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms a
e) 

isInline :: (a, SpecType) -> Either (a, F.Expr) (a, SpecType) 
isInline :: (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) 

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 Reft -> Maybe Expr
F.isSingletonReft (RReft -> Reft
forall r. UReft r -> r
ur_reft RReft
rr) of 
                             Just Expr
e  -> Expr -> Either Expr SpecType
forall a b. a -> Either a b
Left Expr
e
                             Maybe Expr
Nothing -> SpecType -> Either Expr SpecType
forall a b. b -> Either a b
Right (SpecType -> RReft -> SpecType
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   = SpecType -> (RReft -> SpecType) -> Maybe RReft -> SpecType
forall b a. b -> (a -> b) -> Maybe a -> b
maybe SpecType
t' (SpecType -> RReft -> SpecType
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'        = (RReft -> RReft) -> SpecType -> SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RReft -> RReft -> RReft
forall a b. a -> b -> a
const (Reft -> RReft
forall r. r -> UReft r
uTop Reft
forall a. Monoid a => a
mempty)) SpecType
t
    ro :: Maybe RReft
ro        = SpecType -> Maybe RReft
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 <- Maybe SpecType -> [SpecType]
forall a. Maybe a -> [a]
maybeToList (Symbol -> HashMap Symbol SpecType -> Maybe SpecType
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
x HashMap Symbol SpecType
m), SpecType -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
ok 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 -> [Symbol]
deps Symbol
y    = [Symbol] -> (SpecType -> [Symbol]) -> Maybe SpecType -> [Symbol]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (Reft -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms (Reft -> [Symbol]) -> (SpecType -> Reft) -> SpecType -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> Reft
forall r c tv. Reftable r => RType c tv r -> Reft
rTypeReft) (Symbol -> HashMap Symbol SpecType -> Maybe SpecType
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 (Bool -> Bool) -> (RType t t1 t2 -> Bool) -> RType t t1 t2 -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType t t1 t2 -> Bool
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 <- Maybe (WithModel SpecType) -> [WithModel SpecType]
forall a. Maybe a -> [a]
maybeToList (Symbol
-> HashMap Symbol (WithModel SpecType)
-> Maybe (WithModel SpecType)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
x HashMap Symbol (WithModel SpecType)
m), WithModel SpecType -> Bool
forall t t1 t2. WithModel (RType 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 -> [Symbol]
deps Symbol
y    = [Symbol]
-> (WithModel SpecType -> [Symbol])
-> Maybe (WithModel SpecType)
-> [Symbol]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (Reft -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms (Reft -> [Symbol])
-> (WithModel SpecType -> Reft) -> WithModel SpecType -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> Reft
forall r c tv. Reftable r => RType c tv r -> Reft
rTypeReft (SpecType -> Reft)
-> (WithModel SpecType -> SpecType) -> WithModel SpecType -> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithModel SpecType -> SpecType
forall t. WithModel t -> t
dropModel) (Symbol
-> HashMap Symbol (WithModel SpecType)
-> Maybe (WithModel SpecType)
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 (Bool -> Bool)
-> (WithModel (RType t t1 t2) -> Bool)
-> WithModel (RType t t1 t2)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isFunTy (RType t t1 t2 -> Bool)
-> (WithModel (RType t t1 t2) -> RType t t1 t2)
-> WithModel (RType t t1 t2)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithModel (RType t t1 t2) -> RType t t1 t2
forall t. WithModel t -> t
dropModel

expandFix :: (Eq a, Hashable a) => (a -> [a]) -> [a] -> [a]
expandFix :: (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. (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 (a -> HashSet a -> HashSet a
forall a. (Eq 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.Symbol, t)] -> (F.Subst, [(F.Symbol, t)])
tidyTemps :: [(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    = Symbol -> Symbol -> HashMap Symbol Symbol -> Symbol
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      = Subst -> t -> t
forall a. Subable a => Subst -> a -> a
F.subst Subst
θ
    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)]
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       = [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
<$> [Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
n | Integer
n <- [Integer
0 ..]]