{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE DeriveFoldable             #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DeriveTraversable          #-}

module Language.Fixpoint.Horn.Info (
    hornFInfo
  ) where

import qualified Data.HashMap.Strict            as M
import qualified Data.List                      as L
import qualified Data.Tuple                     as Tuple
import qualified Data.Maybe                     as Mb
import           Data.Either                    (partitionEithers)
import           GHC.Generics                   (Generic)
import qualified Language.Fixpoint.Misc         as Misc
import qualified Language.Fixpoint.Types        as F
import qualified Language.Fixpoint.Horn.Types   as H

hornFInfo :: H.Query a -> F.FInfo a
hornFInfo :: Query a -> FInfo a
hornFInfo Query a
q    = GInfo Any a
forall a. Monoid a => a
mempty
  { cm :: HashMap SubcId (SubC a)
F.cm       = HashMap SubcId (SubC a)
cs
  , bs :: BindEnv
F.bs       = BindEnv
be2
  , ebinds :: [BindId]
F.ebinds   = [BindId]
ebs
  , ws :: HashMap KVar (WfC a)
F.ws       = KVEnv a -> HashMap KVar (WfC a)
forall a. KVEnv a -> HashMap KVar (WfC a)
kvEnvWfCs KVEnv a
kve
  , quals :: [Qualifier]
F.quals    = Query a -> [Qualifier]
forall a. Query a -> [Qualifier]
H.qQuals Query a
q
  , gLits :: SEnv Sort
F.gLits    = HashMap Symbol Sort -> SEnv Sort
forall a. HashMap Symbol a -> SEnv a
F.fromMapSEnv (HashMap Symbol Sort -> SEnv Sort)
-> HashMap Symbol Sort -> SEnv Sort
forall a b. (a -> b) -> a -> b
$ Query a -> HashMap Symbol Sort
forall a. Query a -> HashMap Symbol Sort
H.qCon Query a
q
  , dLits :: SEnv Sort
F.dLits    = HashMap Symbol Sort -> SEnv Sort
forall a. HashMap Symbol a -> SEnv a
F.fromMapSEnv (HashMap Symbol Sort -> SEnv Sort)
-> HashMap Symbol Sort -> SEnv Sort
forall a b. (a -> b) -> a -> b
$ Query a -> HashMap Symbol Sort
forall a. Query a -> HashMap Symbol Sort
H.qDis Query a
q
  }
  where
    be0 :: BindEnv
be0        = BindEnv
F.emptyBindEnv
    (BindEnv
be1, KVEnv a
kve) = BindEnv -> [Var a] -> (BindEnv, KVEnv a)
forall a. BindEnv -> [Var a] -> (BindEnv, KVEnv a)
hornWfs   BindEnv
be0     (Query a -> [Var a]
forall a. Query a -> [Var a]
H.qVars Query a
q)
    (BindEnv
be2, [BindId]
ebs, HashMap SubcId (SubC a)
cs) = BindEnv
-> KVEnv a
-> Cstr a
-> (BindEnv, [BindId], HashMap SubcId (SubC a))
forall a.
BindEnv
-> KVEnv a
-> Cstr a
-> (BindEnv, [BindId], HashMap SubcId (SubC a))
hornSubCs BindEnv
be1 KVEnv a
kve Cstr a
hCst
    hCst :: Cstr a
hCst       = Query a -> Cstr a
forall a. Query a -> Cstr a
H.qCstr Query a
q

----------------------------------------------------------------------------------
hornSubCs :: F.BindEnv -> KVEnv a -> H.Cstr a
          -> (F.BindEnv, [F.BindId], M.HashMap F.SubcId (F.SubC a))
----------------------------------------------------------------------------------
hornSubCs :: BindEnv
-> KVEnv a
-> Cstr a
-> (BindEnv, [BindId], HashMap SubcId (SubC a))
hornSubCs BindEnv
be KVEnv a
kve Cstr a
c = (BindEnv
be', [BindId]
ebs, [(SubcId, SubC a)] -> HashMap SubcId (SubC a)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([SubC a] -> [(SubcId, SubC a)]
forall a. [SubC a] -> [(SubcId, SubC a)]
F.addIds [SubC a]
cs))
  where
    (BindEnv
be', [BindId]
ebs, [SubC a]
cs)      = KVEnv a
-> IBindEnv
-> SortedReft
-> BindEnv
-> Cstr a
-> (BindEnv, [BindId], [SubC a])
forall a.
KVEnv a
-> IBindEnv
-> SortedReft
-> BindEnv
-> Cstr a
-> (BindEnv, [BindId], [SubC a])
goS KVEnv a
kve IBindEnv
F.emptyIBindEnv SortedReft
lhs0 BindEnv
be Cstr a
c
    lhs0 :: SortedReft
lhs0           = KVEnv a -> Bind -> SortedReft
forall a. KVEnv a -> Bind -> SortedReft
bindSortedReft KVEnv a
kve Bind
H.dummyBind

-- | @goS@ recursively traverses the NNF constraint to build up a list
--   of the vanilla @SubC@ constraints.

goS :: KVEnv a -> F.IBindEnv -> F.SortedReft -> F.BindEnv -> H.Cstr a
    -> (F.BindEnv, [F.BindId], [F.SubC a])

goS :: KVEnv a
-> IBindEnv
-> SortedReft
-> BindEnv
-> Cstr a
-> (BindEnv, [BindId], [SubC a])
goS KVEnv a
kve IBindEnv
env SortedReft
lhs BindEnv
be Cstr a
c = (BindEnv
be', [BindId]
mEbs, [SubC a]
subcs)
  where
    (BindEnv
be', [Either BindId (SubC a)]
ecs) = KVEnv a
-> IBindEnv
-> SortedReft
-> BindEnv
-> Cstr a
-> (BindEnv, [Either BindId (SubC a)])
forall a.
KVEnv a
-> IBindEnv
-> SortedReft
-> BindEnv
-> Cstr a
-> (BindEnv, [Either BindId (SubC a)])
goS' KVEnv a
kve IBindEnv
env SortedReft
lhs BindEnv
be Cstr a
c
    ([BindId]
mEbs, [SubC a]
subcs) = [Either BindId (SubC a)] -> ([BindId], [SubC a])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either BindId (SubC a)]
ecs

goS' :: KVEnv a -> F.IBindEnv -> F.SortedReft -> F.BindEnv -> H.Cstr a
    -> (F.BindEnv, [Either F.BindId (F.SubC a)])
goS' :: KVEnv a
-> IBindEnv
-> SortedReft
-> BindEnv
-> Cstr a
-> (BindEnv, [Either BindId (SubC a)])
goS' KVEnv a
kve IBindEnv
env SortedReft
lhs BindEnv
be (H.Head Pred
p a
l) = (BindEnv
be, [SubC a -> Either BindId (SubC a)
forall a b. b -> Either a b
Right SubC a
subc])
  where
    subc :: SubC a
subc                        = IBindEnv
-> SortedReft
-> SortedReft
-> Maybe SubcId
-> [BindId]
-> a
-> SubC a
forall a.
IBindEnv
-> SortedReft
-> SortedReft
-> Maybe SubcId
-> [BindId]
-> a
-> SubC a
F.mkSubC IBindEnv
env SortedReft
lhs SortedReft
rhs Maybe SubcId
forall a. Maybe a
Nothing [] a
l
    rhs :: SortedReft
rhs                         = KVEnv a -> SortedReft -> Pred -> SortedReft
forall a. KVEnv a -> SortedReft -> Pred -> SortedReft
updSortedReft KVEnv a
kve SortedReft
lhs Pred
p

goS' KVEnv a
kve IBindEnv
env SortedReft
lhs BindEnv
be (H.CAnd [Cstr a]
cs)  = (BindEnv
be', [[Either BindId (SubC a)]] -> [Either BindId (SubC a)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Either BindId (SubC a)]]
subcss)
  where
    (BindEnv
be', [[Either BindId (SubC a)]]
subcss)               = (BindEnv -> Cstr a -> (BindEnv, [Either BindId (SubC a)]))
-> BindEnv -> [Cstr a] -> (BindEnv, [[Either BindId (SubC a)]])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
L.mapAccumL (KVEnv a
-> IBindEnv
-> SortedReft
-> BindEnv
-> Cstr a
-> (BindEnv, [Either BindId (SubC a)])
forall a.
KVEnv a
-> IBindEnv
-> SortedReft
-> BindEnv
-> Cstr a
-> (BindEnv, [Either BindId (SubC a)])
goS' KVEnv a
kve IBindEnv
env SortedReft
lhs) BindEnv
be [Cstr a]
cs

goS' KVEnv a
kve IBindEnv
env SortedReft
_   BindEnv
be (H.All Bind
b Cstr a
c)  = (BindEnv
be'', [Either BindId (SubC a)]
subcs)
  where
    (BindEnv
be'', [Either BindId (SubC a)]
subcs)               = KVEnv a
-> IBindEnv
-> SortedReft
-> BindEnv
-> Cstr a
-> (BindEnv, [Either BindId (SubC a)])
forall a.
KVEnv a
-> IBindEnv
-> SortedReft
-> BindEnv
-> Cstr a
-> (BindEnv, [Either BindId (SubC a)])
goS' KVEnv a
kve IBindEnv
env' SortedReft
bSR BindEnv
be' Cstr a
c
    (BindId
bId, BindEnv
be')                  = Symbol -> SortedReft -> BindEnv -> (BindId, BindEnv)
F.insertBindEnv (Bind -> Symbol
H.bSym Bind
b) SortedReft
bSR BindEnv
be
    bSR :: SortedReft
bSR                         = KVEnv a -> Bind -> SortedReft
forall a. KVEnv a -> Bind -> SortedReft
bindSortedReft KVEnv a
kve Bind
b
    env' :: IBindEnv
env'                        = [BindId] -> IBindEnv -> IBindEnv
F.insertsIBindEnv [BindId
bId] IBindEnv
env

goS' KVEnv a
kve IBindEnv
env SortedReft
_   BindEnv
be (H.Any Bind
b Cstr a
c)  = (BindEnv
be'', BindId -> Either BindId (SubC a)
forall a b. a -> Either a b
Left BindId
bId Either BindId (SubC a)
-> [Either BindId (SubC a)] -> [Either BindId (SubC a)]
forall a. a -> [a] -> [a]
: [Either BindId (SubC a)]
subcs)
  where
    (BindEnv
be'', [Either BindId (SubC a)]
subcs)               = KVEnv a
-> IBindEnv
-> SortedReft
-> BindEnv
-> Cstr a
-> (BindEnv, [Either BindId (SubC a)])
forall a.
KVEnv a
-> IBindEnv
-> SortedReft
-> BindEnv
-> Cstr a
-> (BindEnv, [Either BindId (SubC a)])
goS' KVEnv a
kve IBindEnv
env' SortedReft
bSR BindEnv
be' Cstr a
c
    (BindId
bId, BindEnv
be')                  = Symbol -> SortedReft -> BindEnv -> (BindId, BindEnv)
F.insertBindEnv (Bind -> Symbol
H.bSym Bind
b) SortedReft
bSR BindEnv
be
    bSR :: SortedReft
bSR                         = KVEnv a -> Bind -> SortedReft
forall a. KVEnv a -> Bind -> SortedReft
bindSortedReft KVEnv a
kve Bind
b
    env' :: IBindEnv
env'                        = [BindId] -> IBindEnv -> IBindEnv
F.insertsIBindEnv [BindId
bId] IBindEnv
env

bindSortedReft :: KVEnv a -> H.Bind -> F.SortedReft
bindSortedReft :: KVEnv a -> Bind -> SortedReft
bindSortedReft KVEnv a
kve (H.Bind Symbol
x Sort
t Pred
p) = Sort -> Reft -> SortedReft
F.RR Sort
t ((Symbol, Expr) -> Reft
F.Reft (Symbol
x, KVEnv a -> Pred -> Expr
forall a. KVEnv a -> Pred -> Expr
predExpr KVEnv a
kve Pred
p))

updSortedReft :: KVEnv a -> F.SortedReft -> H.Pred -> F.SortedReft
updSortedReft :: KVEnv a -> SortedReft -> Pred -> SortedReft
updSortedReft KVEnv a
kve (F.RR Sort
s (F.Reft (Symbol
v, Expr
_))) Pred
p = Sort -> Reft -> SortedReft
F.RR Sort
s ((Symbol, Expr) -> Reft
F.Reft (Symbol
v, KVEnv a -> Pred -> Expr
forall a. KVEnv a -> Pred -> Expr
predExpr KVEnv a
kve Pred
p))

predExpr :: KVEnv a -> H.Pred -> F.Expr
predExpr :: KVEnv a -> Pred -> Expr
predExpr KVEnv a
kve        = Pred -> Expr
go
  where
    go :: Pred -> Expr
go (H.Reft  Expr
e ) = Expr
e
    go (H.Var Symbol
k [Symbol]
ys) = KVEnv a -> Symbol -> [Symbol] -> Expr
forall a. KVEnv a -> Symbol -> [Symbol] -> Expr
kvApp KVEnv a
kve Symbol
k [Symbol]
ys
    go (H.PAnd  [Pred]
ps) = [Expr] -> Expr
F.PAnd (Pred -> Expr
go (Pred -> Expr) -> [Pred] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)

kvApp :: KVEnv a -> F.Symbol -> [F.Symbol] -> F.Expr
kvApp :: KVEnv a -> Symbol -> [Symbol] -> Expr
kvApp KVEnv a
kve Symbol
k [Symbol]
ys = KVar -> Subst -> Expr
F.PKVar (Symbol -> KVar
F.KV Symbol
k) Subst
su
  where
    su :: Subst
su         = [(Symbol, Expr)] -> Subst
F.mkSubst ([Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
params (Symbol -> Expr
forall a. Symbolic a => a -> Expr
F.eVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
ys))
    params :: [Symbol]
params     = [Symbol] -> Maybe [Symbol] -> [Symbol]
forall a. a -> Maybe a -> a
Mb.fromMaybe [Symbol]
forall a. a
err1 (Maybe [Symbol] -> [Symbol]) -> Maybe [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ KVInfo a -> [Symbol]
forall a. KVInfo a -> [Symbol]
kvParams (KVInfo a -> [Symbol]) -> Maybe (KVInfo a) -> Maybe [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> KVEnv a -> Maybe (KVInfo a)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
k KVEnv a
kve
    err1 :: a
err1       = String -> a
forall a. String -> a
F.panic (String
"Unknown Horn variable: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. PPrint a => a -> String
F.showpp Symbol
k)

----------------------------------------------------------------------------------
hornWfs :: F.BindEnv -> [H.Var a] -> (F.BindEnv, KVEnv a)
----------------------------------------------------------------------------------
hornWfs :: BindEnv -> [Var a] -> (BindEnv, KVEnv a)
hornWfs BindEnv
be [Var a]
vars = (BindEnv
be', KVEnv a
kve)
  where
    kve :: KVEnv a
kve         = [(Symbol, KVInfo a)] -> KVEnv a
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (KVInfo a -> Symbol
forall a. KVInfo a -> Symbol
kname KVInfo a
i, KVInfo a
i) | KVInfo a
i <- [KVInfo a]
is ]
    (BindEnv
be', [KVInfo a]
is)   = (BindEnv -> Var a -> (BindEnv, KVInfo a))
-> BindEnv -> [Var a] -> (BindEnv, [KVInfo a])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
L.mapAccumL BindEnv -> Var a -> (BindEnv, KVInfo a)
forall a. BindEnv -> Var a -> (BindEnv, KVInfo a)
kvInfo BindEnv
be [Var a]
vars
    kname :: KVInfo a -> Symbol
kname       = Var a -> Symbol
forall a. Var a -> Symbol
H.hvName (Var a -> Symbol) -> (KVInfo a -> Var a) -> KVInfo a -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KVInfo a -> Var a
forall a. KVInfo a -> Var a
kvVar

kvInfo :: F.BindEnv -> H.Var a -> (F.BindEnv, KVInfo a)
kvInfo :: BindEnv -> Var a -> (BindEnv, KVInfo a)
kvInfo BindEnv
be Var a
k       = (BindEnv
be', Var a -> [Symbol] -> WfC a -> KVInfo a
forall a. Var a -> [Symbol] -> WfC a -> KVInfo a
KVInfo Var a
k ((Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
xts) WfC a
wfc)
  where
    -- make the WfC
    wfc :: WfC a
wfc           = IBindEnv -> (Symbol, Sort, KVar) -> a -> WfC a
forall a. IBindEnv -> (Symbol, Sort, KVar) -> a -> WfC a
F.WfC IBindEnv
wenv (Symbol, Sort, KVar)
wrft  (Var a -> a
forall a. Var a -> a
H.hvMeta Var a
k)
    wenv :: IBindEnv
wenv          = [BindId] -> IBindEnv
F.fromListIBindEnv [BindId]
ids
    wrft :: (Symbol, Sort, KVar)
wrft          = (Symbol
x, Sort
t, Symbol -> KVar
F.KV (Var a -> Symbol
forall a. Var a -> Symbol
H.hvName Var a
k))
    -- add the binders
    (BindEnv
be', [BindId]
ids)    = (BindEnv -> (Symbol, Sort) -> (BindEnv, BindId))
-> BindEnv -> [(Symbol, Sort)] -> (BindEnv, [BindId])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
L.mapAccumL BindEnv -> (Symbol, Sort) -> (BindEnv, BindId)
insertBE BindEnv
be [(Symbol, Sort)]
xts'
    ((Symbol
x,Sort
t), [(Symbol, Sort)]
xts') = String -> [(Symbol, Sort)] -> ((Symbol, Sort), [(Symbol, Sort)])
forall a.
(?callStack::CallStack) =>
String -> ListNE a -> (a, ListNE a)
Misc.safeUncons String
"Horn var with no args" [(Symbol, Sort)]
xts
    -- make the parameters
    xts :: [(Symbol, Sort)]
xts           = [ (Var a -> BindId -> Symbol
forall a. Var a -> BindId -> Symbol
hvarArg Var a
k BindId
i, Sort
t) | (Sort
t, BindId
i) <- [Sort] -> [BindId] -> [(Sort, BindId)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Var a -> [Sort]
forall a. Var a -> [Sort]
H.hvArgs Var a
k) [BindId
0..] ]

insertBE :: F.BindEnv -> (F.Symbol, F.Sort) -> (F.BindEnv, F.BindId)
insertBE :: BindEnv -> (Symbol, Sort) -> (BindEnv, BindId)
insertBE BindEnv
be (Symbol
x, Sort
t) = (BindId, BindEnv) -> (BindEnv, BindId)
forall a b. (a, b) -> (b, a)
Tuple.swap ((BindId, BindEnv) -> (BindEnv, BindId))
-> (BindId, BindEnv) -> (BindEnv, BindId)
forall a b. (a -> b) -> a -> b
$ Symbol -> SortedReft -> BindEnv -> (BindId, BindEnv)
F.insertBindEnv Symbol
x (Sort -> SortedReft
F.trueSortedReft Sort
t) BindEnv
be

----------------------------------------------------------------------------------
-- | Data types and helpers for manipulating information about KVars
----------------------------------------------------------------------------------
type KVEnv a  = M.HashMap F.Symbol (KVInfo a)

data KVInfo a = KVInfo
  { KVInfo a -> Var a
kvVar    :: !(H.Var a)
  , KVInfo a -> [Symbol]
kvParams :: ![F.Symbol]
  , KVInfo a -> WfC a
kvWfC    :: !(F.WfC a)
  }
  deriving ((forall x. KVInfo a -> Rep (KVInfo a) x)
-> (forall x. Rep (KVInfo a) x -> KVInfo a) -> Generic (KVInfo a)
forall x. Rep (KVInfo a) x -> KVInfo a
forall x. KVInfo a -> Rep (KVInfo a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (KVInfo a) x -> KVInfo a
forall a x. KVInfo a -> Rep (KVInfo a) x
$cto :: forall a x. Rep (KVInfo a) x -> KVInfo a
$cfrom :: forall a x. KVInfo a -> Rep (KVInfo a) x
Generic, a -> KVInfo b -> KVInfo a
(a -> b) -> KVInfo a -> KVInfo b
(forall a b. (a -> b) -> KVInfo a -> KVInfo b)
-> (forall a b. a -> KVInfo b -> KVInfo a) -> Functor KVInfo
forall a b. a -> KVInfo b -> KVInfo a
forall a b. (a -> b) -> KVInfo a -> KVInfo b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> KVInfo b -> KVInfo a
$c<$ :: forall a b. a -> KVInfo b -> KVInfo a
fmap :: (a -> b) -> KVInfo a -> KVInfo b
$cfmap :: forall a b. (a -> b) -> KVInfo a -> KVInfo b
Functor)

kvEnvWfCs :: KVEnv a -> M.HashMap F.KVar (F.WfC a)
kvEnvWfCs :: KVEnv a -> HashMap KVar (WfC a)
kvEnvWfCs KVEnv a
kve = [(KVar, WfC a)] -> HashMap KVar (WfC a)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (Symbol -> KVar
F.KV Symbol
k, KVInfo a -> WfC a
forall a. KVInfo a -> WfC a
kvWfC KVInfo a
info) | (Symbol
k, KVInfo a
info) <- KVEnv a -> [(Symbol, KVInfo a)]
forall k v. HashMap k v -> [(k, v)]
M.toList KVEnv a
kve ]

hvarArg :: H.Var a -> Int -> F.Symbol
hvarArg :: Var a -> BindId -> Symbol
hvarArg Var a
k BindId
i = Symbol -> BindId -> Symbol
forall a. Show a => Symbol -> a -> Symbol
F.intSymbol (Symbol -> Symbol -> Symbol
F.suffixSymbol Symbol
hvarPrefix (Var a -> Symbol
forall a. Var a -> Symbol
H.hvName Var a
k)) BindId
i

hvarPrefix :: F.Symbol
hvarPrefix :: Symbol
hvarPrefix = String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol String
"nnf_arg"