{-# 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           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.Types.Config as F
import qualified Language.Fixpoint.Horn.Types   as H
import Data.Maybe (fromMaybe)

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

axEnv :: F.Config -> H.Query a -> M.HashMap F.SubcId b -> F.AxiomEnv
axEnv :: forall a b. Config -> Query a -> HashMap SubcId b -> AxiomEnv
axEnv Config
cfg Query a
q HashMap SubcId b
cs = forall a. Monoid a => a
mempty
  { aenvEqs :: [Equation]
F.aenvEqs    = forall a. Query a -> [Equation]
H.qEqns Query a
q
  , aenvSimpl :: [Rewrite]
F.aenvSimpl  = forall a. Query a -> [Rewrite]
H.qMats Query a
q
  , aenvExpand :: HashMap SubcId Bool
F.aenvExpand = if Config -> Bool
F.rewriteAxioms Config
cfg then Bool
True forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ HashMap SubcId b
cs else forall a. Monoid a => a
mempty
  }

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

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

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

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

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

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

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

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

myMkSubC :: F.IBindEnv -> Maybe F.SortedReft -> F.SortedReft -> Maybe Integer -> F.Tag -> a -> F.SubC a
myMkSubC :: forall a.
IBindEnv
-> Maybe SortedReft
-> SortedReft
-> Maybe SubcId
-> [BindId]
-> a
-> SubC a
myMkSubC IBindEnv
be Maybe SortedReft
lhsMb SortedReft
rhs Maybe SubcId
x [BindId]
y a
z = forall a.
IBindEnv
-> SortedReft
-> SortedReft
-> Maybe SubcId
-> [BindId]
-> a
-> SubC a
F.mkSubC IBindEnv
be SortedReft
lhs SortedReft
rhs Maybe SubcId
x [BindId]
y a
z
  where
    lhs :: SortedReft
lhs = forall a. a -> Maybe a -> a
fromMaybe SortedReft
def Maybe SortedReft
lhsMb
    def :: SortedReft
def = Sort -> SortedReft
F.trueSortedReft (SortedReft -> Sort
F.sr_sort SortedReft
rhs)

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

updSortedReft :: KVEnv a -> Maybe F.SortedReft -> H.Pred -> F.SortedReft
updSortedReft :: forall a. KVEnv a -> Maybe SortedReft -> Pred -> SortedReft
updSortedReft KVEnv a
kve Maybe SortedReft
lhs Pred
p = Sort -> Reft -> SortedReft
F.RR Sort
s ((Symbol, Expr) -> Reft
F.Reft (Symbol
v, forall a. KVEnv a -> Pred -> Expr
predExpr KVEnv a
kve Pred
p))
   where
      (Sort
s, Symbol
v) = case Maybe SortedReft
lhs of
                 Just (F.RR Sort
ss (F.Reft (Symbol
vv, Expr
_))) -> (Sort
ss, Symbol
vv)
                 Maybe SortedReft
Nothing                       -> (Sort
F.intSort, Symbol
F.dummySymbol)

-- dummyBind :: a -> Bind a
-- dummyBind = Bind F.dummySymbol F.intSort (PAnd [])


predExpr :: KVEnv a -> H.Pred -> F.Expr
predExpr :: forall a. 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) = 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)

kvApp :: KVEnv a -> F.Symbol -> [F.Symbol] -> F.Expr
kvApp :: forall a. 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 (forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
params (forall a. Symbolic a => a -> Expr
F.eVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
ys))
    params :: [Symbol]
params     = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall {a}. a
err1 forall a. KVInfo a -> [Symbol]
kvParams (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
k KVEnv a
kve)
    err1 :: a
err1       = forall a. String -> a
F.panic (String
"Unknown Horn variable: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp Symbol
k)

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

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

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

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

data KVInfo a = KVInfo
  { forall a. KVInfo a -> Var a
kvVar    :: !(H.Var a)
  , forall a. KVInfo a -> [Symbol]
kvParams :: ![F.Symbol]
  , forall a. KVInfo a -> WfC a
kvWfC    :: !(F.WfC a)
  }
  deriving (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, 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
<$ :: forall a b. a -> KVInfo b -> KVInfo a
$c<$ :: forall a b. a -> KVInfo b -> KVInfo a
fmap :: forall a b. (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 :: forall a. KVEnv a -> HashMap KVar (WfC a)
kvEnvWfCs KVEnv a
kve = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (Symbol -> KVar
F.KV Symbol
k, forall a. KVInfo a -> WfC a
kvWfC KVInfo a
info) | (Symbol
k, KVInfo a
info) <- forall k v. HashMap k v -> [(k, v)]
M.toList KVEnv a
kve ]

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

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