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

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

import           Control.Monad (forM)
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.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 :: [Int]
F.ebinds    = [Int]
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 forall a. [a] -> [a] -> [a]
++ forall a. Scrape -> Cstr a -> [Qualifier]
scrapeCstr (Config -> Scrape
F.scrape Config
cfg) Cstr a
hCst
  , 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, [Int]
ebs, HashMap SubcId (SubC a)
cs) = 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           = 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, [Int], HashMap SubcId (SubC a))
hornSubCs BindEnv a
be KVEnv a
kve Cstr a
c = (BindEnv a
be', [Int]
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', [Int]
ebs, [SubC a]
cs) = 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) = forall a.
KVEnv a
-> IBindEnv
-> Maybe SortedReft
-> BindEnv a
-> Cstr a
-> (BindEnv a, [Either Int (SubC a)])
goS' KVEnv a
kve IBindEnv
env forall a. Maybe a
Nothing BindEnv a
be Cstr a
c
    ([Int]
mEbs, [SubC a]
subcs) = 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, [forall a b. b -> Either a b
Right SubC a
subc])
  where
    subc :: SubC a
subc                        = forall a.
IBindEnv
-> Maybe SortedReft
-> SortedReft
-> Maybe SubcId
-> [Int]
-> 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 Int (SubC a)]]
subcss)
  where
    (BindEnv a
be', [[Either Int (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 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)               = forall a.
KVEnv a
-> IBindEnv
-> Maybe SortedReft
-> BindEnv a
-> Cstr a
-> (BindEnv a, [Either Int (SubC a)])
goS' KVEnv a
kve IBindEnv
env' (forall a. a -> Maybe a
Just SortedReft
bSR) BindEnv a
be' Cstr a
c
    (Int
bId, BindEnv a
be')                  = forall a.
Symbol -> SortedReft -> a -> BindEnv a -> (Int, 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'                        = [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'', forall a b. a -> Either a b
Left Int
bId forall a. a -> [a] -> [a]
: [Either Int (SubC a)]
subcs)
  where
    (BindEnv a
be'', [Either Int (SubC a)]
subcs)               = forall a.
KVEnv a
-> IBindEnv
-> Maybe SortedReft
-> BindEnv a
-> Cstr a
-> (BindEnv a, [Either Int (SubC a)])
goS' KVEnv a
kve IBindEnv
env' (forall a. a -> Maybe a
Just SortedReft
bSR) BindEnv a
be' Cstr a
c
    (Int
bId, BindEnv a
be')                  = forall a.
Symbol -> SortedReft -> a -> BindEnv a -> (Int, 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'                        = [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 = 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 = 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, 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)

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          = [Int] -> IBindEnv
F.fromListIBindEnv [Int]
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', [Int]
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, Int)
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 -> Int -> Symbol
hvarArg Var a
k Int
i, Sort
t', a
a) | (Sort
t', Int
i) <- forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Var a -> [Sort]
H.hvArgs Var a
k) [Int
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, Int)
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 -> (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 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 -> Int -> Symbol
hvarArg Var a
k Int
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)) Int
i

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

-------------------------------------------------------------------------------
-- | 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 = forall a. Ord a => [a] -> [a]
Misc.sortNub forall a b. (a -> b) -> a -> b
$ 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)  = 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)  = forall a. Scrape -> BindEnv -> Bind a -> [Qualifier]
scrapeBind Scrape
m BindEnv
senv' Bind a
b forall a. Semigroup a => a -> a -> a
<> BindEnv -> Cstr a -> [Qualifier]
go BindEnv
senv' Cstr a
c where senv' :: BindEnv
senv' = forall a. Bind a -> BindEnv -> BindEnv
insertBindEnv Bind a
b BindEnv
senv
    go BindEnv
senv (H.Any Bind a
b Cstr a
c)  = forall a. Scrape -> BindEnv -> Bind a -> [Qualifier]
scrapeBind Scrape
m BindEnv
senv' Bind a
b forall a. Semigroup a => a -> a -> a
<> BindEnv -> Cstr a -> [Qualifier]
go BindEnv
senv' Cstr a
c where senv' :: BindEnv
senv' = 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 (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) = 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 Expr
e)  = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (BindEnv -> Expr -> [Qualifier]
mkQual BindEnv
senv) (Expr -> [Expr]
F.concConjuncts Expr
e)

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

mkScrapeQual :: [(F.Symbol, F.Sort)] -> F.Expr -> F.Qualifier
mkScrapeQual :: [(Symbol, Sort)] -> Expr -> Qualifier
mkScrapeQual [(Symbol, Sort)]
xts Expr
e = Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
F.mkQual (forall a. Symbolic a => a -> Symbol
F.symbol String
"AUTO") [QualParam]
qParams (forall a. Subable a => Subst -> a -> a
F.subst Subst
su Expr
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    = 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 :: Subst
su      = [(Symbol, Expr)] -> Subst
F.mkSubst [ (Symbol
x, forall a. Expression a => a -> Expr
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 forall a. Ord a => a -> a -> Bool
<= Int
maxQualifierParams = forall a. Int -> [a] -> [[a]]
recycle Int
n [(Symbol, Sort)]
xts
  | Bool
otherwise              = []
  where
    n :: Int
n                      = 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
xforall a. a -> [a] -> [a]
:[a]
xs) forall a. a -> [a] -> [a]
: forall a. Int -> [a] -> [[a]]
recycle (Int
kforall a. Num a => a -> a -> a
-Int
1) ([a]
xs 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 -> Expr -> Maybe [(Symbol, Sort)]
qualParams BindEnv
env Expr
e = do
    let xs :: [Symbol]
xs = forall a. Eq a => [a] -> [a]
Misc.nubOrd (forall a. Subable a => a -> [Symbol]
F.syms Expr
e)
    [(Int, Symbol, Sort)]
ixts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Symbol]
xs forall a b. (a -> b) -> a -> b
$ \Symbol
x -> do
              (Sort
t, Int
i) <- Symbol -> BindEnv -> Maybe (Sort, Int)
lookupBindEnv Symbol
x BindEnv
env
              forall (m :: * -> *) a. Monad m => a -> m a
return (Int
i, Symbol
x, Sort
t)
    forall (m :: * -> *) a. Monad m => a -> m a
return [ (Symbol
x, Sort
t) | (Int
_, Symbol
x, Sort
t) <- forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
L.sort forall a b. (a -> b) -> a -> b
$ [(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 = 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 forall a. Num a => a -> a -> a
+ Int
1, bBinds :: HashMap Symbol (Sort, Int)
bBinds = 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 = forall a. Bind a -> Symbol
H.bSym Bind a
b
    t :: Sort
t = 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 = 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)