{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DeriveTraversable          #-}

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

import           Control.Monad (forM)
import           Data.Ord (Down(..), comparing)
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 qualified Data.Maybe                     as Mb

hornFInfo :: (F.Fixpoint a, F.PPrint a) => F.Config -> H.Query a -> F.FInfo a
hornFInfo :: forall a. (Fixpoint a, PPrint a) => Config -> Query a -> FInfo a
hornFInfo Config
cfg Query a
q = GInfo Any a
forall a. Monoid a => a
mempty
  { F.cm        = cs
  , F.bs        = be2
  , F.ebinds    = ebs
  , F.ws        = kvEnvWfCs kve
  , F.quals     = H.qQuals q ++ scrapeCstr (F.scrape cfg) hCst
  , F.gLits     = F.fromMapSEnv $ H.qCon q
  , F.dLits     = F.fromMapSEnv $ H.qDis q
  , F.ae        = axEnv cfg q cs
  , F.ddecls    = H.qData q
  , F.hoInfo    = F.cfgHoInfo cfg
  }
  where
    be0 :: BindEnv a
be0         = BindEnv a
forall a. BindEnv a
F.emptyBindEnv
    (BindEnv a
be1, KVEnv a
kve)  = BindEnv a -> [Var a] -> (BindEnv a, KVEnv a)
forall a. PPrint a => BindEnv a -> [Var a] -> (BindEnv a, KVEnv a)
hornWfs   BindEnv a
forall a. BindEnv a
be0     (Query a -> [Var a]
forall a. Query a -> [Var a]
H.qVars Query a
q)
    (BindEnv a
be2, [Int]
ebs, HashMap SubcId (SubC a)
cs) = BindEnv a
-> KVEnv a -> Cstr a -> (BindEnv a, [Int], HashMap SubcId (SubC a))
forall a.
BindEnv a
-> KVEnv a -> Cstr a -> (BindEnv a, [Int], HashMap SubcId (SubC a))
hornSubCs BindEnv a
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


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 = AxiomEnv
forall a. Monoid a => a
mempty
  { F.aenvEqs    = H.qEqns q
  , F.aenvSimpl  = H.qMats q
  , F.aenvExpand = if F.rewriteAxioms cfg then True <$ cs else 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, [Int], HashMap SubcId (SubC a))
hornSubCs BindEnv a
be KVEnv a
kve Cstr a
c = (BindEnv a
be', [Int]
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 a
be', [Int]
ebs, [SubC a]
cs) = KVEnv a
-> IBindEnv -> BindEnv a -> Cstr a -> (BindEnv a, [Int], [SubC a])
forall a.
KVEnv a
-> IBindEnv -> BindEnv a -> Cstr a -> (BindEnv a, [Int], [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, [Int], [SubC a])
goS KVEnv a
kve IBindEnv
env BindEnv a
be Cstr a
c = (BindEnv a
be', [Int]
mEbs, [SubC a]
subcs)
  where
    (BindEnv a
be', [Either Int (SubC a)]
ecs) = KVEnv a
-> IBindEnv
-> Maybe SortedReft
-> BindEnv a
-> Cstr a
-> (BindEnv a, [Either Int (SubC a)])
forall a.
KVEnv a
-> IBindEnv
-> Maybe SortedReft
-> BindEnv a
-> Cstr a
-> (BindEnv a, [Either Int (SubC a)])
goS' KVEnv a
kve IBindEnv
env Maybe SortedReft
forall a. Maybe a
Nothing BindEnv a
be Cstr a
c
    ([Int]
mEbs, [SubC a]
subcs) = [Either Int (SubC a)] -> ([Int], [SubC a])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either Int (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 Int (SubC a)])
goS' KVEnv a
kve IBindEnv
env Maybe SortedReft
lhs BindEnv a
be (H.Head Pred
p a
l) = (BindEnv a
be, [SubC a -> Either Int (SubC a)
forall a b. b -> Either a b
Right SubC a
subc])
  where
    subc :: SubC a
subc                        = IBindEnv
-> Maybe SortedReft
-> SortedReft
-> Maybe SubcId
-> [Int]
-> a
-> SubC a
forall a.
IBindEnv
-> Maybe SortedReft
-> SortedReft
-> Maybe SubcId
-> [Int]
-> a
-> SubC a
myMkSubC IBindEnv
env Maybe SortedReft
lhs SortedReft
rhs Maybe SubcId
forall a. Maybe a
Nothing [] a
l
    rhs :: SortedReft
rhs                         = KVEnv a -> Maybe SortedReft -> Pred -> SortedReft
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', [[Either Int (SubC a)]] -> [Either Int (SubC a)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Either Int (SubC a)]]
subcss)
  where
    (BindEnv a
be', [[Either Int (SubC a)]]
subcss)               = (BindEnv a -> Cstr a -> (BindEnv a, [Either Int (SubC a)]))
-> BindEnv a -> [Cstr a] -> (BindEnv a, [[Either Int (SubC a)]])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
L.mapAccumL (KVEnv a
-> IBindEnv
-> Maybe SortedReft
-> BindEnv a
-> Cstr a
-> (BindEnv a, [Either Int (SubC a)])
forall a.
KVEnv a
-> IBindEnv
-> Maybe SortedReft
-> BindEnv a
-> Cstr a
-> (BindEnv a, [Either Int (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 Int (SubC a)]
subcs)
  where
    (BindEnv a
be'', [Either Int (SubC a)]
subcs)               = KVEnv a
-> IBindEnv
-> Maybe SortedReft
-> BindEnv a
-> Cstr a
-> (BindEnv a, [Either Int (SubC a)])
forall a.
KVEnv a
-> IBindEnv
-> Maybe SortedReft
-> BindEnv a
-> Cstr a
-> (BindEnv a, [Either Int (SubC a)])
goS' KVEnv a
kve IBindEnv
env' (SortedReft -> Maybe SortedReft
forall a. a -> Maybe a
Just SortedReft
bSR) BindEnv a
be' Cstr a
c
    (Int
bId, BindEnv a
be')                  = Symbol -> SortedReft -> a -> BindEnv a -> (Int, BindEnv a)
forall a.
Symbol -> SortedReft -> a -> BindEnv a -> (Int, BindEnv a)
F.insertBindEnv (Bind a -> Symbol
forall a. Bind a -> Symbol
H.bSym Bind a
b) SortedReft
bSR (Bind a -> a
forall a. Bind a -> a
H.bMeta Bind a
b) BindEnv a
be
    bSR :: SortedReft
bSR                         = KVEnv a -> Bind a -> SortedReft
forall a. KVEnv a -> Bind a -> SortedReft
bindSortedReft KVEnv a
kve Bind a
b
    env' :: IBindEnv
env'                        = [Int] -> IBindEnv -> IBindEnv
F.insertsIBindEnv [Int
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'', Int -> Either Int (SubC a)
forall a b. a -> Either a b
Left Int
bId Either Int (SubC a)
-> [Either Int (SubC a)] -> [Either Int (SubC a)]
forall a. a -> [a] -> [a]
: [Either Int (SubC a)]
subcs)
  where
    (BindEnv a
be'', [Either Int (SubC a)]
subcs)               = KVEnv a
-> IBindEnv
-> Maybe SortedReft
-> BindEnv a
-> Cstr a
-> (BindEnv a, [Either Int (SubC a)])
forall a.
KVEnv a
-> IBindEnv
-> Maybe SortedReft
-> BindEnv a
-> Cstr a
-> (BindEnv a, [Either Int (SubC a)])
goS' KVEnv a
kve IBindEnv
env' (SortedReft -> Maybe SortedReft
forall a. a -> Maybe a
Just SortedReft
bSR) BindEnv a
be' Cstr a
c
    (Int
bId, BindEnv a
be')                  = Symbol -> SortedReft -> a -> BindEnv a -> (Int, BindEnv a)
forall a.
Symbol -> SortedReft -> a -> BindEnv a -> (Int, BindEnv a)
F.insertBindEnv (Bind a -> Symbol
forall a. Bind a -> Symbol
H.bSym Bind a
b) SortedReft
bSR (Bind a -> a
forall a. Bind a -> a
H.bMeta Bind a
b) BindEnv a
be
    bSR :: SortedReft
bSR                         = KVEnv a -> Bind a -> SortedReft
forall a. KVEnv a -> Bind a -> SortedReft
bindSortedReft KVEnv a
kve Bind a
b
    env' :: IBindEnv
env'                        = [Int] -> IBindEnv -> IBindEnv
F.insertsIBindEnv [Int
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
-> [Int]
-> a
-> SubC a
myMkSubC IBindEnv
be Maybe SortedReft
lhsMb SortedReft
rhs Maybe SubcId
x [Int]
y a
z = IBindEnv
-> SortedReft -> SortedReft -> Maybe SubcId -> [Int] -> a -> SubC a
forall a.
IBindEnv
-> SortedReft -> SortedReft -> Maybe SubcId -> [Int] -> a -> SubC a
F.mkSubC IBindEnv
be SortedReft
lhs SortedReft
rhs Maybe SubcId
x [Int]
y a
z
  where
    lhs :: SortedReft
lhs = SortedReft -> Maybe SortedReft -> SortedReft
forall a. a -> Maybe a -> a
Mb.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, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (Symbol
x, KVEnv a -> Pred -> ExprV Symbol
forall a. KVEnv a -> Pred -> ExprV Symbol
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, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (Symbol
v, KVEnv a -> Pred -> ExprV Symbol
forall a. KVEnv a -> Pred -> ExprV Symbol
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, ExprV Symbol
_))) -> (Sort
ss, Symbol
vv)
                 Maybe SortedReft
Nothing                       -> (Sort
F.intSort, Symbol
F.dummySymbol)

predExpr :: KVEnv a -> H.Pred -> F.Expr
predExpr :: forall a. KVEnv a -> Pred -> ExprV Symbol
predExpr KVEnv a
kve        = Pred -> ExprV Symbol
go
  where
    go :: Pred -> ExprV Symbol
go (H.Reft  ExprV Symbol
e ) = ExprV Symbol
e
    go (H.Var Symbol
k [Symbol]
ys) = KVEnv a -> Symbol -> [Symbol] -> ExprV Symbol
forall a. KVEnv a -> Symbol -> [Symbol] -> ExprV Symbol
kvApp KVEnv a
kve Symbol
k [Symbol]
ys
    go (H.PAnd  [Pred]
ps) = [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
F.PAnd (Pred -> ExprV Symbol
go (Pred -> ExprV Symbol) -> [Pred] -> [ExprV Symbol]
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] -> ExprV Symbol
kvApp KVEnv a
kve Symbol
k [Symbol]
ys = KVar -> SubstV Symbol -> ExprV Symbol
forall v. KVar -> SubstV v -> ExprV v
F.PKVar (Symbol -> KVar
F.KV Symbol
k) SubstV Symbol
su
  where
    su :: SubstV Symbol
su         = [(Symbol, ExprV Symbol)] -> SubstV Symbol
F.mkSubst ([Symbol] -> [ExprV Symbol] -> [(Symbol, ExprV Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
params (Symbol -> ExprV Symbol
forall a. Symbolic a => a -> ExprV Symbol
F.eVar (Symbol -> ExprV Symbol) -> [Symbol] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
ys))
    params :: [Symbol]
params     = [Symbol] -> (KVInfo a -> [Symbol]) -> Maybe (KVInfo a) -> [Symbol]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Symbol]
forall {a}. a
err1 KVInfo a -> [Symbol]
forall a. KVInfo a -> [Symbol]
kvParams (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.PPrint a) => F.BindEnv a -> [H.Var a] -> (F.BindEnv a, KVEnv a)
----------------------------------------------------------------------------------
hornWfs :: forall a. PPrint 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         = [(Symbol, KVInfo a)] -> HashMap Symbol (KVInfo 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 a
be', [KVInfo a]
is)   = (BindEnv a -> Var a -> (BindEnv a, KVInfo a))
-> BindEnv a -> [Var a] -> (BindEnv a, [KVInfo a])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
L.mapAccumL BindEnv a -> Var a -> (BindEnv a, KVInfo a)
forall a. PPrint a => BindEnv a -> Var a -> (BindEnv a, KVInfo a)
kvInfo BindEnv a
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.PPrint a) => F.BindEnv a -> H.Var a -> (F.BindEnv a, KVInfo a)
kvInfo :: forall a. PPrint a => BindEnv a -> Var a -> (BindEnv a, KVInfo a)
kvInfo BindEnv a
be Var a
k       = (BindEnv a
be', Var a -> [Symbol] -> WfC a -> KVInfo a
forall a. Var a -> [Symbol] -> WfC a -> KVInfo a
KVInfo Var a
k ((Symbol, Sort, a) -> Symbol
forall a b c. (a, b, c) -> a
Misc.fst3 ((Symbol, Sort, a) -> Symbol) -> [(Symbol, Sort, a)] -> [Symbol]
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           = 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          = [Int] -> IBindEnv
F.fromListIBindEnv [Int]
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 a
be', [Int]
ids)    = (BindEnv a -> (Symbol, Sort, a) -> (BindEnv a, Int))
-> BindEnv a -> [(Symbol, Sort, a)] -> (BindEnv a, [Int])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
L.mapAccumL BindEnv a -> (Symbol, Sort, a) -> (BindEnv a, Int)
forall a. BindEnv a -> (Symbol, Sort, a) -> (BindEnv a, Int)
insertBE BindEnv a
be [(Symbol, Sort, a)]
xts'
    ((Symbol
x,Sort
t,a
_), [(Symbol, Sort, a)]
xts') = String
-> [(Symbol, Sort, a)] -> ((Symbol, Sort, a), [(Symbol, Sort, a)])
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           = [ (Var a -> Int -> Symbol
forall a. Var a -> Int -> Symbol
hvarArg Var a
k Int
i, Sort
t', a
a) | (Sort
t', Int
i) <- [Sort] -> [Int] -> [(Sort, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Var a -> [Sort]
forall a. Var a -> [Sort]
H.hvArgs Var a
k) [Int
0..] ]
    a :: a
a             = Var 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, Int)
insertBE BindEnv a
be (Symbol
x, Sort
t, a
a) = (Int, BindEnv a) -> (BindEnv a, Int)
forall a b. (a, b) -> (b, a)
Tuple.swap ((Int, BindEnv a) -> (BindEnv a, Int))
-> (Int, BindEnv a) -> (BindEnv a, Int)
forall a b. (a -> b) -> a -> b
$ Symbol -> SortedReft -> a -> BindEnv a -> (Int, BindEnv a)
forall a.
Symbol -> SortedReft -> a -> BindEnv a -> (Int, 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 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
$cfrom :: forall a x. KVInfo a -> Rep (KVInfo a) x
from :: forall x. KVInfo a -> Rep (KVInfo a) x
$cto :: forall a x. Rep (KVInfo a) x -> KVInfo a
to :: forall x. Rep (KVInfo a) x -> KVInfo a
Generic, (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
$cfmap :: forall a b. (a -> b) -> KVInfo a -> KVInfo b
fmap :: forall a b. (a -> b) -> KVInfo a -> KVInfo b
$c<$ :: forall a b. a -> KVInfo b -> KVInfo a
<$ :: forall a b. a -> KVInfo b -> KVInfo a
Functor)

kvEnvWfCs :: KVEnv a -> M.HashMap F.KVar (F.WfC a)
kvEnvWfCs :: forall a. 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 :: forall a. Var a -> Int -> Symbol
hvarArg Var a
k Int
i = Symbol -> Int -> Symbol
F.hvarArgSymbol (Var a -> Symbol
forall a. Var a -> Symbol
H.hvName Var a
k) Int
i

-------------------------------------------------------------------------------
-- | Automatically scrape qualifiers from all predicates in a constraint
-------------------------------------------------------------------------------

scrapeCstr :: F.Scrape -> H.Cstr a -> [F.Qualifier]
scrapeCstr :: forall a. Scrape -> Cstr a -> [Qualifier]
scrapeCstr Scrape
F.No Cstr a
_    = []
scrapeCstr Scrape
m    Cstr a
cstr = [Qualifier] -> [Qualifier]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([Qualifier] -> [Qualifier]) -> [Qualifier] -> [Qualifier]
forall a b. (a -> b) -> a -> b
$ BindEnv -> Cstr a -> [Qualifier]
forall {a}. BindEnv -> Cstr a -> [Qualifier]
go BindEnv
emptyBindEnv Cstr a
cstr
  where
    go :: BindEnv -> Cstr a -> [Qualifier]
go BindEnv
senv (H.Head Pred
p a
_) = BindEnv -> Pred -> [Qualifier]
scrapePred BindEnv
senv Pred
p
    go BindEnv
senv (H.CAnd [Cstr a]
cs)  = (Cstr a -> [Qualifier]) -> [Cstr a] -> [Qualifier]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (BindEnv -> Cstr a -> [Qualifier]
go BindEnv
senv) [Cstr a]
cs
    go BindEnv
senv (H.All Bind a
b Cstr a
c)  = Scrape -> BindEnv -> Bind a -> [Qualifier]
forall a. Scrape -> BindEnv -> Bind a -> [Qualifier]
scrapeBind Scrape
m BindEnv
senv' Bind a
b [Qualifier] -> [Qualifier] -> [Qualifier]
forall a. Semigroup a => a -> a -> a
<> BindEnv -> Cstr a -> [Qualifier]
go BindEnv
senv' Cstr a
c where senv' :: BindEnv
senv' = Bind a -> BindEnv -> BindEnv
forall a. Bind a -> BindEnv -> BindEnv
insertBindEnv Bind a
b BindEnv
senv
    go BindEnv
senv (H.Any Bind a
b Cstr a
c)  = Scrape -> BindEnv -> Bind a -> [Qualifier]
forall a. Scrape -> BindEnv -> Bind a -> [Qualifier]
scrapeBind Scrape
m BindEnv
senv' Bind a
b [Qualifier] -> [Qualifier] -> [Qualifier]
forall a. Semigroup a => a -> a -> a
<> BindEnv -> Cstr a -> [Qualifier]
go BindEnv
senv' Cstr a
c where senv' :: BindEnv
senv' = Bind a -> BindEnv -> BindEnv
forall a. Bind a -> BindEnv -> BindEnv
insertBindEnv Bind a
b BindEnv
senv

scrapeBind :: F.Scrape -> BindEnv -> H.Bind a -> [F.Qualifier]
scrapeBind :: forall a. Scrape -> BindEnv -> Bind a -> [Qualifier]
scrapeBind Scrape
F.Both BindEnv
senv Bind a
b = BindEnv -> Pred -> [Qualifier]
scrapePred BindEnv
senv (Bind a -> Pred
forall a. Bind a -> Pred
H.bPred Bind a
b)
scrapeBind Scrape
_      BindEnv
_    Bind a
_ = []

scrapePred :: BindEnv -> H.Pred -> [F.Qualifier]
scrapePred :: BindEnv -> Pred -> [Qualifier]
scrapePred BindEnv
_    (H.Var Symbol
_ [Symbol]
_) = []
scrapePred BindEnv
senv (H.PAnd [Pred]
ps) = (Pred -> [Qualifier]) -> [Pred] -> [Qualifier]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (BindEnv -> Pred -> [Qualifier]
scrapePred BindEnv
senv) [Pred]
ps
scrapePred BindEnv
senv (H.Reft ExprV Symbol
e)  = (ExprV Symbol -> [Qualifier]) -> [ExprV Symbol] -> [Qualifier]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (BindEnv -> ExprV Symbol -> [Qualifier]
mkQual BindEnv
senv) (ExprV Symbol -> [ExprV Symbol]
F.concConjuncts ExprV Symbol
e)

-- NOTE: Constraints.mkQual will do extra stuff like generalizing the sorts...
mkQual :: BindEnv -> F.Expr -> [ F.Qualifier ]
mkQual :: BindEnv -> ExprV Symbol -> [Qualifier]
mkQual BindEnv
env ExprV Symbol
e = case BindEnv -> ExprV Symbol -> Maybe [(Symbol, Sort)]
qualParams BindEnv
env ExprV Symbol
e of
  Maybe [(Symbol, Sort)]
Nothing  -> []
  Just [(Symbol, Sort)]
xts -> [ [(Symbol, Sort)] -> ExprV Symbol -> Qualifier
mkScrapeQual [(Symbol, Sort)]
xts' ExprV Symbol
e | [(Symbol, Sort)]
xts' <- [(Symbol, Sort)] -> [[(Symbol, Sort)]]
shiftCycle [(Symbol, Sort)]
xts ]

mkScrapeQual :: [(F.Symbol, F.Sort)] -> F.Expr -> F.Qualifier
mkScrapeQual :: [(Symbol, Sort)] -> ExprV Symbol -> Qualifier
mkScrapeQual [(Symbol, Sort)]
xts ExprV Symbol
e = Symbol -> [QualParam] -> ExprV Symbol -> SourcePos -> Qualifier
forall v.
Symbol -> [QualParam] -> ExprV v -> SourcePos -> QualifierV v
F.mkQual (String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol String
"AUTO") [QualParam]
qParams (SubstV Symbol -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => SubstV Symbol -> a -> a
F.subst SubstV Symbol
su ExprV Symbol
e) (String -> SourcePos
F.dummyPos String
"")
  where
    qParams :: [QualParam]
qParams = [ F.QP {qpSym :: Symbol
F.qpSym = Symbol
y, qpPat :: QualPattern
F.qpPat = QualPattern
F.PatNone, qpSort :: Sort
F.qpSort = Sort
t} | (Symbol
_, Symbol
y, Sort
t) <- [(Symbol, Symbol, Sort)]
xyts ]
    xyts :: [(Symbol, Symbol, Sort)]
xyts    = (SubcId -> (Symbol, Sort) -> (Symbol, Symbol, Sort))
-> [SubcId] -> [(Symbol, Sort)] -> [(Symbol, Symbol, Sort)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\SubcId
i (Symbol
x, Sort
t) -> (Symbol
x, SubcId -> Symbol
F.bindSymbol SubcId
i, Sort
t)) [SubcId
0..] [(Symbol, Sort)]
xts
    su :: SubstV Symbol
su      = [(Symbol, ExprV Symbol)] -> SubstV Symbol
F.mkSubst [ (Symbol
x, Symbol -> ExprV Symbol
forall a. Expression a => a -> ExprV Symbol
F.expr Symbol
y) | (Symbol
x, Symbol
y, Sort
_) <- [(Symbol, Symbol, Sort)]
xyts ]


shiftCycle :: [(F.Symbol, F.Sort)] -> [[(F.Symbol, F.Sort)]]
shiftCycle :: [(Symbol, Sort)] -> [[(Symbol, Sort)]]
shiftCycle [(Symbol, Sort)]
xts
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
maxQualifierParams = Int -> [(Symbol, Sort)] -> [[(Symbol, Sort)]]
forall a. Int -> [a] -> [[a]]
recycle Int
n [(Symbol, Sort)]
xts
  | Bool
otherwise              = []
  where
    n :: Int
n                      = [(Symbol, Sort)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, Sort)]
xts

recycle :: Int -> [a] -> [[a]]
recycle :: forall a. Int -> [a] -> [[a]]
recycle Int
0 [a]
_      = []
recycle Int
_ []     = []
recycle Int
k (a
x:[a]
xs) = (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs) [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: Int -> [a] -> [[a]]
forall a. Int -> [a] -> [[a]]
recycle (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) ([a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a
x])

maxQualifierParams :: Int
maxQualifierParams :: Int
maxQualifierParams = Int
3

{-
  1. Normalize the names
  2. Permute the args?
 -}

qualParams :: BindEnv -> F.Expr -> Maybe [(F.Symbol, F.Sort)]
qualParams :: BindEnv -> ExprV Symbol -> Maybe [(Symbol, Sort)]
qualParams BindEnv
env ExprV Symbol
e = do
    let xs :: [Symbol]
xs = [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a]
Misc.nubOrd (ExprV Symbol -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms ExprV Symbol
e)
    [(Int, Symbol, Sort)]
ixts <- [Symbol]
-> (Symbol -> Maybe (Int, Symbol, Sort))
-> Maybe [(Int, Symbol, Sort)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Symbol]
xs ((Symbol -> Maybe (Int, Symbol, Sort))
 -> Maybe [(Int, Symbol, Sort)])
-> (Symbol -> Maybe (Int, Symbol, Sort))
-> Maybe [(Int, Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ \Symbol
x -> do
              (Sort
t, Int
i) <- Symbol -> BindEnv -> Maybe (Sort, Int)
lookupBindEnv Symbol
x BindEnv
env
              (Int, Symbol, Sort) -> Maybe (Int, Symbol, Sort)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
i, Symbol
x, Sort
t)
    [(Symbol, Sort)] -> Maybe [(Symbol, Sort)]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [ (Symbol
x, Sort
t) | (Int
_, Symbol
x, Sort
t) <- ((Int, Symbol, Sort) -> (Int, Symbol, Sort) -> Ordering)
-> [(Int, Symbol, Sort)] -> [(Int, Symbol, Sort)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
L.sortBy (((Int, Symbol, Sort) -> Down (Int, Symbol, Sort))
-> (Int, Symbol, Sort) -> (Int, Symbol, Sort) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Int, Symbol, Sort) -> Down (Int, Symbol, Sort)
forall a. a -> Down a
Down) [(Int, Symbol, Sort)]
ixts ]

    -- ixts = [ (i, x, t) | x <- xs, (i, t) <- lookupBindEnv x env ]

-------------------------------------------------------------------------------

-- | `BindEnv` maps each symbol to (sort, depth) pair, where shorter depths
--    means bound "earlier" i.e. in (forall (x1:...) (forall (x2:...) ...)
--    the depth of x1 is less than the depth of x2.
--    We use the heuristic that the symbol with the "largest" depth is the
--    "value-variable" in the qualifier.

data BindEnv = BindEnv
  { BindEnv -> Int
bSize  :: !Int
  , BindEnv -> HashMap Symbol (Sort, Int)
bBinds :: M.HashMap F.Symbol (F.Sort, Int)
  }

emptyBindEnv :: BindEnv
emptyBindEnv :: BindEnv
emptyBindEnv = BindEnv { bSize :: Int
bSize = Int
0, bBinds :: HashMap Symbol (Sort, Int)
bBinds = HashMap Symbol (Sort, Int)
forall a. Monoid a => a
mempty }

insertBindEnv :: H.Bind a -> BindEnv -> BindEnv
insertBindEnv :: forall a. Bind a -> BindEnv -> BindEnv
insertBindEnv Bind a
b BindEnv
senv = BindEnv { bSize :: Int
bSize = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, bBinds :: HashMap Symbol (Sort, Int)
bBinds = Symbol
-> (Sort, Int)
-> HashMap Symbol (Sort, Int)
-> HashMap Symbol (Sort, Int)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
x (Sort
t, Int
n) (BindEnv -> HashMap Symbol (Sort, Int)
bBinds BindEnv
senv) }
  where
    n :: Int
n = BindEnv -> Int
bSize BindEnv
senv
    x :: Symbol
x = Bind a -> Symbol
forall a. Bind a -> Symbol
H.bSym Bind a
b
    t :: Sort
t = Bind a -> Sort
forall a. Bind a -> Sort
H.bSort Bind a
b

lookupBindEnv :: F.Symbol -> BindEnv -> Maybe (F.Sort, Int)
lookupBindEnv :: Symbol -> BindEnv -> Maybe (Sort, Int)
lookupBindEnv Symbol
x BindEnv
env = Symbol -> HashMap Symbol (Sort, Int) -> Maybe (Sort, Int)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
x (BindEnv -> HashMap Symbol (Sort, Int)
bBinds BindEnv
env)