{-# LANGUAGE CPP                        #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NoMonomorphismRestriction  #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE PatternGuards              #-}

{-# OPTIONS_GHC -Wno-name-shadowing     #-}

-- | This module contains the top-level QUERY data types and elements,
--   including (Horn) implication & well-formedness constraints and sets.
module Language.Fixpoint.Types.Constraints (

   -- * Top-level Queries
    FInfo, SInfo, GInfo (..), FInfoWithOpts(..)
  , convertFormat
  , sinfoToFInfo
  , Solver

   -- * Serializing
  , toFixpoint
  , writeFInfo
  , saveQuery

   -- * Constructing Queries
  , fi

  -- * Constraints
  , WfC (..), isGWfc, updateWfCExpr
  , SubC, SubcId
  , mkSubC, subcId, sid, senv, updateSEnv, slhs, srhs, stag, subC, wfC
  , SimpC (..)
  , Tag
  , TaggedC, clhs, crhs
  -- , strengthenLhs
  , strengthenHyp
  , strengthenBinds

  -- * Accessing Constraints
  , addIds
  , sinfo
  , shiftVV
  , gwInfo, GWInfo (..)

  -- * Qualifiers
  , Qualifier   (..)
  , QualParam   (..)
  , QualPattern (..)
  , trueQual
  , qualifier
  , mkQual
  , remakeQual
  , mkQ
  , qualBinds

  -- * Results
  , FixSolution
  , GFixSolution, toGFixSol
  , Result (..)
  , unsafe, isUnsafe, isSafe ,safe

  -- * Cut KVars
  , Kuts (..)
  , ksMember

  -- * Higher Order Logic
  , HOInfo (..)
  , allowHO
  , allowHOquals

  -- * Axioms
  , AxiomEnv (..)
  , Equation (..)
  , mkEquation
  , Rewrite  (..)
  , AutoRewrite (..)
  , dedupAutoRewrites

  -- * Misc  [should be elsewhere but here due to dependencies]
  , substVars
  , sortVars
  , gSorts
  ) where

import qualified Data.Store as S
import           Data.Generics             (Data)
import           Data.Aeson                hiding (Result)
import qualified Data.Set                  as Set
import           Data.Typeable             (Typeable)
import           Data.Hashable
import           GHC.Generics              (Generic)
import qualified Data.List                 as L -- (sort, nub, delete)
import           Data.Maybe                (catMaybes)
import           Control.DeepSeq
import           Control.Monad             (void)
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Config hiding (allowHO)
import           Language.Fixpoint.Types.Triggers
import           Language.Fixpoint.Types.Names
import           Language.Fixpoint.Types.Errors
import           Language.Fixpoint.Types.Spans
import           Language.Fixpoint.Types.Sorts
import           Language.Fixpoint.Types.Refinements
import           Language.Fixpoint.Types.Substitutions
import           Language.Fixpoint.Types.Environments
import qualified Language.Fixpoint.Utils.Files as Files
import qualified Language.Fixpoint.Solver.Stats as Solver

import           Language.Fixpoint.Misc
import           Text.PrettyPrint.HughesPJ.Compat
import qualified Data.HashMap.Strict       as M
import qualified Data.HashSet              as S
import qualified Data.ByteString           as B
import qualified Data.Binary as B

--------------------------------------------------------------------------------
-- | Constraints ---------------------------------------------------------------
--------------------------------------------------------------------------------

{-@ type Tag = { v : [Int] | len v == 1 } @-}

type Tag           = [Int]

data WfC a  =  WfC  { forall a. WfC a -> IBindEnv
wenv  :: !IBindEnv
                    , forall a. WfC a -> (Symbol, Sort, KVar)
wrft  :: (Symbol, Sort, KVar)
                    , forall a. WfC a -> a
winfo :: !a
                    }
             | GWfC { wenv  :: !IBindEnv
                    , wrft  :: !(Symbol, Sort, KVar)
                    , winfo :: !a
                    , forall a. WfC a -> Expr
wexpr :: !Expr
                    , forall a. WfC a -> GradInfo
wloc  :: !GradInfo
                    }
              deriving (WfC a -> WfC a -> Bool
forall a. Eq a => WfC a -> WfC a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WfC a -> WfC a -> Bool
$c/= :: forall a. Eq a => WfC a -> WfC a -> Bool
== :: WfC a -> WfC a -> Bool
$c== :: forall a. Eq a => WfC a -> WfC a -> Bool
Eq, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (WfC a) x -> WfC a
forall a x. WfC a -> Rep (WfC a) x
$cto :: forall a x. Rep (WfC a) x -> WfC a
$cfrom :: forall a x. WfC a -> Rep (WfC a) x
Generic, forall a b. a -> WfC b -> WfC a
forall a b. (a -> b) -> WfC a -> WfC 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 -> WfC b -> WfC a
$c<$ :: forall a b. a -> WfC b -> WfC a
fmap :: forall a b. (a -> b) -> WfC a -> WfC b
$cfmap :: forall a b. (a -> b) -> WfC a -> WfC b
Functor)

data GWInfo = GWInfo { GWInfo -> Symbol
gsym  :: Symbol
                     , GWInfo -> Sort
gsort :: Sort
                     , GWInfo -> Expr
gexpr :: Expr
                     , GWInfo -> GradInfo
ginfo :: GradInfo
                     }
              deriving (GWInfo -> GWInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GWInfo -> GWInfo -> Bool
$c/= :: GWInfo -> GWInfo -> Bool
== :: GWInfo -> GWInfo -> Bool
$c== :: GWInfo -> GWInfo -> Bool
Eq, forall x. Rep GWInfo x -> GWInfo
forall x. GWInfo -> Rep GWInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep GWInfo x -> GWInfo
$cfrom :: forall x. GWInfo -> Rep GWInfo x
Generic)

gwInfo :: WfC a -> GWInfo
gwInfo :: forall a. WfC a -> GWInfo
gwInfo (GWfC IBindEnv
_ (Symbol
x,Sort
s,KVar
_) a
_ Expr
e GradInfo
i)
  = Symbol -> Sort -> Expr -> GradInfo -> GWInfo
GWInfo Symbol
x Sort
s Expr
e GradInfo
i
gwInfo WfC a
_
  = forall a. (?callStack::CallStack) => [Char] -> a
errorstar [Char]
"gwInfo"

updateWfCExpr :: (Expr -> Expr) -> WfC a -> WfC a
updateWfCExpr :: forall a. (Expr -> Expr) -> WfC a -> WfC a
updateWfCExpr Expr -> Expr
_ w :: WfC a
w@WfC{}  = WfC a
w
updateWfCExpr Expr -> Expr
f w :: WfC a
w@GWfC{} = WfC a
w{wexpr :: Expr
wexpr = Expr -> Expr
f (forall a. WfC a -> Expr
wexpr WfC a
w)}

isGWfc :: WfC a -> Bool
isGWfc :: forall a. WfC a -> Bool
isGWfc GWfC{} = Bool
True
isGWfc WfC{}  = Bool
False

instance HasGradual (WfC a) where
  isGradual :: WfC a -> Bool
isGradual = forall a. WfC a -> Bool
isGWfc

type SubcId = Integer

data SubC a = SubC
  { forall a. SubC a -> IBindEnv
_senv  :: !IBindEnv
  , forall a. SubC a -> SortedReft
slhs   :: !SortedReft
  , forall a. SubC a -> SortedReft
srhs   :: !SortedReft
  , forall a. SubC a -> Maybe SubcId
_sid   :: !(Maybe SubcId)
  , forall a. SubC a -> [BindId]
_stag  :: !Tag
  , forall a. SubC a -> a
_sinfo :: !a
  }
  deriving (SubC a -> SubC a -> Bool
forall a. Eq a => SubC a -> SubC a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SubC a -> SubC a -> Bool
$c/= :: forall a. Eq a => SubC a -> SubC a -> Bool
== :: SubC a -> SubC a -> Bool
$c== :: forall a. Eq a => SubC a -> SubC a -> Bool
Eq, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (SubC a) x -> SubC a
forall a x. SubC a -> Rep (SubC a) x
$cto :: forall a x. Rep (SubC a) x -> SubC a
$cfrom :: forall a x. SubC a -> Rep (SubC a) x
Generic, forall a b. a -> SubC b -> SubC a
forall a b. (a -> b) -> SubC a -> SubC 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 -> SubC b -> SubC a
$c<$ :: forall a b. a -> SubC b -> SubC a
fmap :: forall a b. (a -> b) -> SubC a -> SubC b
$cfmap :: forall a b. (a -> b) -> SubC a -> SubC b
Functor)

data SimpC a = SimpC
  { forall a. SimpC a -> IBindEnv
_cenv  :: !IBindEnv
  , forall a. SimpC a -> Expr
_crhs  :: !Expr
  , forall a. SimpC a -> Maybe SubcId
_cid   :: !(Maybe Integer)
  , forall a. SimpC a -> BindId
cbind  :: !BindId               -- ^ Id of lhs/rhs binder
  , forall a. SimpC a -> [BindId]
_ctag  :: !Tag
  , forall a. SimpC a -> a
_cinfo :: !a
  }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (SimpC a) x -> SimpC a
forall a x. SimpC a -> Rep (SimpC a) x
$cto :: forall a x. Rep (SimpC a) x -> SimpC a
$cfrom :: forall a x. SimpC a -> Rep (SimpC a) x
Generic, forall a b. a -> SimpC b -> SimpC a
forall a b. (a -> b) -> SimpC a -> SimpC 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 -> SimpC b -> SimpC a
$c<$ :: forall a b. a -> SimpC b -> SimpC a
fmap :: forall a b. (a -> b) -> SimpC a -> SimpC b
$cfmap :: forall a b. (a -> b) -> SimpC a -> SimpC b
Functor)

instance Loc a => Loc (SimpC a) where
  srcSpan :: SimpC a -> SrcSpan
srcSpan = forall a. Loc a => a -> SrcSpan
srcSpan forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SimpC a -> a
_cinfo

strengthenHyp :: SInfo a -> [(Integer, Expr)] -> SInfo a
strengthenHyp :: forall a. SInfo a -> [(SubcId, Expr)] -> SInfo a
strengthenHyp SInfo a
si [(SubcId, Expr)]
ies = forall a. SInfo a -> HashMap BindId Expr -> SInfo a
strengthenBinds SInfo a
si HashMap BindId Expr
bindExprs
  where
    bindExprs :: HashMap BindId Expr
bindExprs        = forall k v.
(?callStack::CallStack, Eq k, Hashable k, Show k) =>
[Char] -> [(k, v)] -> HashMap k v
safeFromList [Char]
"strengthenHyp" [ (forall a. SInfo a -> SubcId -> BindId
subcBind SInfo a
si SubcId
i, Expr
e) | (SubcId
i, Expr
e) <- [(SubcId, Expr)]
ies ]

subcBind :: SInfo a -> SubcId -> BindId
subcBind :: forall a. SInfo a -> SubcId -> BindId
subcBind SInfo a
si SubcId
i
  | Just SimpC a
c <- forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup SubcId
i (forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
si)
  = forall a. SimpC a -> BindId
cbind SimpC a
c
  | Bool
otherwise
  = forall a. (?callStack::CallStack) => [Char] -> a
errorstar forall a b. (a -> b) -> a -> b
$ [Char]
"Unknown subcId in subcBind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show SubcId
i


strengthenBinds :: SInfo a -> M.HashMap BindId Expr -> SInfo a
strengthenBinds :: forall a. SInfo a -> HashMap BindId Expr -> SInfo a
strengthenBinds SInfo a
si HashMap BindId Expr
m = SInfo a
si { bs :: BindEnv a
bs = forall a.
(BindId -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a))
-> BindEnv a -> BindEnv a
mapBindEnv BindId -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a)
f (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
si) }
  where
    f :: BindId -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a)
f BindId
i (Symbol
x, SortedReft
sr, a
l)   = case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup BindId
i HashMap BindId Expr
m of
                         Maybe Expr
Nothing -> (Symbol
x, SortedReft
sr, a
l)
                         Just Expr
e  -> (Symbol
x, SortedReft -> Expr -> SortedReft
strengthenSortedReft SortedReft
sr Expr
e, a
l)

strengthenSortedReft :: SortedReft -> Expr -> SortedReft
strengthenSortedReft :: SortedReft -> Expr -> SortedReft
strengthenSortedReft (RR Sort
s (Reft (Symbol
v, Expr
r))) Expr
e = Sort -> Reft -> SortedReft
RR Sort
s ((Symbol, Expr) -> Reft
Reft (Symbol
v, [Expr] -> Expr
pAnd [Expr
r, Expr
e]))


{-
  [(Int, Expr)]  ==> [(BindId, Expr)]

 -}

-- strengthenLhs :: Expr -> SubC a -> SubC a
-- strengthenLhs e subc = subc {slhs = go (slhs subc)}
--  where
--    go (RR s (Reft(v, r))) = RR s (Reft (v, pAnd [r, e]))

class TaggedC c a where
  senv  :: c a -> IBindEnv
  updateSEnv  :: c a -> (IBindEnv -> IBindEnv) -> c a
  sid   :: c a -> Maybe Integer
  stag  :: c a -> Tag
  sinfo :: c a -> a
  clhs  :: BindEnv a -> c a -> [(Symbol, SortedReft)]
  crhs  :: c a -> Expr

instance TaggedC SimpC a where
  senv :: SimpC a -> IBindEnv
senv      = forall a. SimpC a -> IBindEnv
_cenv
  updateSEnv :: SimpC a -> (IBindEnv -> IBindEnv) -> SimpC a
updateSEnv SimpC a
c IBindEnv -> IBindEnv
f = SimpC a
c { _cenv :: IBindEnv
_cenv = IBindEnv -> IBindEnv
f (forall a. SimpC a -> IBindEnv
_cenv SimpC a
c) }
  sid :: SimpC a -> Maybe SubcId
sid       = forall a. SimpC a -> Maybe SubcId
_cid
  stag :: SimpC a -> [BindId]
stag      = forall a. SimpC a -> [BindId]
_ctag
  sinfo :: SimpC a -> a
sinfo     = forall a. SimpC a -> a
_cinfo
  crhs :: SimpC a -> Expr
crhs      = forall a. SimpC a -> Expr
_crhs
  clhs :: BindEnv a -> SimpC a -> [(Symbol, SortedReft)]
clhs BindEnv a
be SimpC a
c = forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
envCs BindEnv a
be (forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC a
c)

instance TaggedC SubC a where
  senv :: SubC a -> IBindEnv
senv      = forall a. SubC a -> IBindEnv
_senv
  updateSEnv :: SubC a -> (IBindEnv -> IBindEnv) -> SubC a
updateSEnv SubC a
c IBindEnv -> IBindEnv
f = SubC a
c { _senv :: IBindEnv
_senv = IBindEnv -> IBindEnv
f (forall a. SubC a -> IBindEnv
_senv SubC a
c) }
  sid :: SubC a -> Maybe SubcId
sid       = forall a. SubC a -> Maybe SubcId
_sid
  stag :: SubC a -> [BindId]
stag      = forall a. SubC a -> [BindId]
_stag
  sinfo :: SubC a -> a
sinfo     = forall a. SubC a -> a
_sinfo
  crhs :: SubC a -> Expr
crhs      = Reft -> Expr
reftPred forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SubC a -> SortedReft
srhs
  clhs :: BindEnv a -> SubC a -> [(Symbol, SortedReft)]
clhs BindEnv a
be SubC a
c = SortedReft -> (Symbol, SortedReft)
sortedReftBind (forall a. SubC a -> SortedReft
slhs SubC a
c) forall a. a -> [a] -> [a]
: forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
envCs BindEnv a
be (forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
c)

sortedReftBind :: SortedReft -> (Symbol, SortedReft)
sortedReftBind :: SortedReft -> (Symbol, SortedReft)
sortedReftBind SortedReft
sr = (Symbol
x, SortedReft
sr)
  where
    Reft (Symbol
x, Expr
_)   = SortedReft -> Reft
sr_reft SortedReft
sr

subcId :: (TaggedC c a) => c a -> SubcId
subcId :: forall (c :: * -> *) a. TaggedC c a => c a -> SubcId
subcId = forall a. (?callStack::CallStack) => [Char] -> Maybe a -> a
mfromJust [Char]
"subCId" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid

---------------------------------------------------------------------------
-- | Solutions and Results
---------------------------------------------------------------------------

type GFixSolution = GFixSol Expr

type FixSolution  = M.HashMap KVar Expr

newtype GFixSol e = GSol (M.HashMap KVar (e, [e]))
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (GFixSol e) x -> GFixSol e
forall e x. GFixSol e -> Rep (GFixSol e) x
$cto :: forall e x. Rep (GFixSol e) x -> GFixSol e
$cfrom :: forall e x. GFixSol e -> Rep (GFixSol e) x
Generic, NonEmpty (GFixSol e) -> GFixSol e
GFixSol e -> GFixSol e -> GFixSol e
forall b. Integral b => b -> GFixSol e -> GFixSol e
forall e. NonEmpty (GFixSol e) -> GFixSol e
forall e. GFixSol e -> GFixSol e -> GFixSol e
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall e b. Integral b => b -> GFixSol e -> GFixSol e
stimes :: forall b. Integral b => b -> GFixSol e -> GFixSol e
$cstimes :: forall e b. Integral b => b -> GFixSol e -> GFixSol e
sconcat :: NonEmpty (GFixSol e) -> GFixSol e
$csconcat :: forall e. NonEmpty (GFixSol e) -> GFixSol e
<> :: GFixSol e -> GFixSol e -> GFixSol e
$c<> :: forall e. GFixSol e -> GFixSol e -> GFixSol e
Semigroup, GFixSol e
[GFixSol e] -> GFixSol e
GFixSol e -> GFixSol e -> GFixSol e
forall e. Semigroup (GFixSol e)
forall e. GFixSol e
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall e. [GFixSol e] -> GFixSol e
forall e. GFixSol e -> GFixSol e -> GFixSol e
mconcat :: [GFixSol e] -> GFixSol e
$cmconcat :: forall e. [GFixSol e] -> GFixSol e
mappend :: GFixSol e -> GFixSol e -> GFixSol e
$cmappend :: forall e. GFixSol e -> GFixSol e -> GFixSol e
mempty :: GFixSol e
$cmempty :: forall e. GFixSol e
Monoid, forall a b. a -> GFixSol b -> GFixSol a
forall a b. (a -> b) -> GFixSol a -> GFixSol 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 -> GFixSol b -> GFixSol a
$c<$ :: forall a b. a -> GFixSol b -> GFixSol a
fmap :: forall a b. (a -> b) -> GFixSol a -> GFixSol b
$cfmap :: forall a b. (a -> b) -> GFixSol a -> GFixSol b
Functor)

toGFixSol :: M.HashMap KVar (e, [e]) -> GFixSol e
toGFixSol :: forall e. HashMap KVar (e, [e]) -> GFixSol e
toGFixSol = forall e. HashMap KVar (e, [e]) -> GFixSol e
GSol


data Result a = Result
  { forall a. Result a -> FixResult a
resStatus    :: !(FixResult a)
  , forall a. Result a -> FixSolution
resSolution  :: !FixSolution
  , forall a. Result a -> FixSolution
resNonCutsSolution :: !FixSolution
  , forall a. Result a -> GFixSolution
gresSolution :: !GFixSolution
  }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Result a) x -> Result a
forall a x. Result a -> Rep (Result a) x
$cto :: forall a x. Rep (Result a) x -> Result a
$cfrom :: forall a x. Result a -> Rep (Result a) x
Generic, BindId -> Result a -> ShowS
forall a. Show a => BindId -> Result a -> ShowS
forall a. Show a => [Result a] -> ShowS
forall a. Show a => Result a -> [Char]
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Result a] -> ShowS
$cshowList :: forall a. Show a => [Result a] -> ShowS
show :: Result a -> [Char]
$cshow :: forall a. Show a => Result a -> [Char]
showsPrec :: BindId -> Result a -> ShowS
$cshowsPrec :: forall a. Show a => BindId -> Result a -> ShowS
Show, forall a b. a -> Result b -> Result a
forall a b. (a -> b) -> Result a -> Result 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 -> Result b -> Result a
$c<$ :: forall a b. a -> Result b -> Result a
fmap :: forall a b. (a -> b) -> Result a -> Result b
$cfmap :: forall a b. (a -> b) -> Result a -> Result b
Functor)



instance ToJSON a => ToJSON (Result a) where
  toJSON :: Result a -> Value
toJSON = forall a. ToJSON a => a -> Value
toJSON forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Result a -> FixResult a
resStatus

instance Semigroup (Result a) where
  Result a
r1 <> :: Result a -> Result a -> Result a
<> Result a
r2  = forall a.
FixResult a
-> FixSolution -> FixSolution -> GFixSolution -> Result a
Result FixResult a
stat FixSolution
soln FixSolution
nonCutsSoln GFixSolution
gsoln
    where
      stat :: FixResult a
stat  = forall a. Result a -> FixResult a
resStatus Result a
r1    forall a. Semigroup a => a -> a -> a
<> forall a. Result a -> FixResult a
resStatus Result a
r2
      soln :: FixSolution
soln  = forall a. Result a -> FixSolution
resSolution Result a
r1  forall a. Semigroup a => a -> a -> a
<> forall a. Result a -> FixSolution
resSolution Result a
r2
      nonCutsSoln :: FixSolution
nonCutsSoln = forall a. Result a -> FixSolution
resNonCutsSolution Result a
r1 forall a. Semigroup a => a -> a -> a
<> forall a. Result a -> FixSolution
resNonCutsSolution Result a
r2
      gsoln :: GFixSolution
gsoln = forall a. Result a -> GFixSolution
gresSolution Result a
r1 forall a. Semigroup a => a -> a -> a
<> forall a. Result a -> GFixSolution
gresSolution Result a
r2

instance Monoid (Result a) where
  mempty :: Result a
mempty        = forall a.
FixResult a
-> FixSolution -> FixSolution -> GFixSolution -> Result a
Result forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
  mappend :: Result a -> Result a -> Result a
mappend       = forall a. Semigroup a => a -> a -> a
(<>)

unsafe, safe :: Result a
unsafe :: forall a. Result a
unsafe = forall a. Monoid a => a
mempty {resStatus :: FixResult a
resStatus = forall a. Stats -> [a] -> FixResult a
Unsafe forall a. Monoid a => a
mempty []}
safe :: forall a. Result a
safe   = forall a. Monoid a => a
mempty {resStatus :: FixResult a
resStatus = forall a. Stats -> FixResult a
Safe forall a. Monoid a => a
mempty}

isSafe :: Result a -> Bool
isSafe :: forall a. Result a -> Bool
isSafe Result a
r = case forall a. Result a -> FixResult a
resStatus Result a
r of
  Safe{} -> Bool
True
  FixResult a
_ -> Bool
False

isUnsafe :: Result a -> Bool
isUnsafe :: forall a. Result a -> Bool
isUnsafe Result a
r | Unsafe Stats
_ [a]
_ <- forall a. Result a -> FixResult a
resStatus Result a
r
  = Bool
True
isUnsafe Result a
_ = Bool
False

instance (Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a)) where
  toFix :: FixResult (SubC a) -> Doc
toFix (Safe Stats
stats)     = [Char] -> Doc
text [Char]
"Safe (" Doc -> Doc -> Doc
<+> [Char] -> Doc
text (forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Stats -> BindId
Solver.checked Stats
stats) Doc -> Doc -> Doc
<+> Doc
" constraints checked)"
  -- toFix (UnknownError d) = text $ "Unknown Error: " ++ d
  toFix (Crash [(SubC a, Maybe [Char])]
xs [Char]
msg)   = [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ [ [Char] -> Doc
text [Char]
"Crash!" ] forall a. [a] -> [a] -> [a]
++  forall a. (Ord a, Fixpoint a) => [Char] -> [SubC a] -> [Doc]
pprSinfos [Char]
"CRASH: " (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SubC a, Maybe [Char])]
xs) forall a. [a] -> [a] -> [a]
++ [Doc -> Doc
parens ([Char] -> Doc
text [Char]
msg)]
  toFix (Unsafe Stats
_ [SubC a]
xs)    = [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
text [Char]
"Unsafe:" forall a. a -> [a] -> [a]
: forall a. (Ord a, Fixpoint a) => [Char] -> [SubC a] -> [Doc]
pprSinfos [Char]
"WARNING: " [SubC a]
xs

pprSinfos :: (Ord a, Fixpoint a) => String -> [SubC a] -> [Doc]
pprSinfos :: forall a. (Ord a, Fixpoint a) => [Char] -> [SubC a] -> [Doc]
pprSinfos [Char]
msg = forall a b. (a -> b) -> [a] -> [b]
map (([Char] -> Doc
text [Char]
msg Doc -> Doc -> Doc
<->) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fixpoint a => a -> Doc
toFix) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
L.sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo

instance Fixpoint a => Show (WfC a) where
  show :: WfC a -> [Char]
show = forall a. Fixpoint a => a -> [Char]
showFix

instance Fixpoint a => Show (SubC a) where
  show :: SubC a -> [Char]
show = forall a. Fixpoint a => a -> [Char]
showFix

instance Fixpoint a => Show (SimpC a) where
  show :: SimpC a -> [Char]
show = forall a. Fixpoint a => a -> [Char]
showFix

instance Fixpoint a => PPrint (SubC a) where
  pprintTidy :: Tidy -> SubC a -> Doc
pprintTidy Tidy
_ = forall a. Fixpoint a => a -> Doc
toFix

instance Fixpoint a => PPrint (SimpC a) where
  pprintTidy :: Tidy -> SimpC a -> Doc
pprintTidy Tidy
_ = forall a. Fixpoint a => a -> Doc
toFix

instance Fixpoint a => PPrint (WfC a) where
  pprintTidy :: Tidy -> WfC a -> Doc
pprintTidy Tidy
_ = forall a. Fixpoint a => a -> Doc
toFix

instance Fixpoint a => Fixpoint (SubC a) where
  toFix :: SubC a -> Doc
toFix SubC a
c     = Doc -> BindId -> Doc -> Doc
hang ([Char] -> Doc
text [Char]
"\n\nconstraint:") BindId
2 Doc
bd
     where bd :: Doc
bd =   forall a. Fixpoint a => a -> Doc
toFix (forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
c)
              Doc -> Doc -> Doc
$+$ [Char] -> Doc
text [Char]
"lhs" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix (forall a. SubC a -> SortedReft
slhs SubC a
c)
              Doc -> Doc -> Doc
$+$ [Char] -> Doc
text [Char]
"rhs" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix (forall a. SubC a -> SortedReft
srhs SubC a
c)
              Doc -> Doc -> Doc
$+$ (forall a. Show a => Maybe a -> Doc
pprId (forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid SubC a
c) Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"tag" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix (forall (c :: * -> *) a. TaggedC c a => c a -> [BindId]
stag SubC a
c))
              Doc -> Doc -> Doc
$+$ Doc -> Doc -> Doc
toFixMeta ([Char] -> Doc
text [Char]
"constraint" Doc -> Doc -> Doc
<+> forall a. Show a => Maybe a -> Doc
pprId (forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid SubC a
c)) (forall a. Fixpoint a => a -> Doc
toFix (forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SubC a
c))

instance Fixpoint a => Fixpoint (SimpC a) where
  toFix :: SimpC a -> Doc
toFix SimpC a
c     = Doc -> BindId -> Doc -> Doc
hang ([Char] -> Doc
text [Char]
"\n\nsimpleConstraint:") BindId
2 Doc
bd
     where bd :: Doc
bd =   forall a. Fixpoint a => a -> Doc
toFix (forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC a
c)
              Doc -> Doc -> Doc
$+$ [Char] -> Doc
text [Char]
"rhs" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix (forall (c :: * -> *) a. TaggedC c a => c a -> Expr
crhs SimpC a
c)
              Doc -> Doc -> Doc
$+$ (forall a. Show a => Maybe a -> Doc
pprId (forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid SimpC a
c) Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"tag" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix (forall (c :: * -> *) a. TaggedC c a => c a -> [BindId]
stag SimpC a
c))
              Doc -> Doc -> Doc
$+$ Doc -> Doc -> Doc
toFixMeta ([Char] -> Doc
text [Char]
"simpleConstraint" Doc -> Doc -> Doc
<+> forall a. Show a => Maybe a -> Doc
pprId (forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid SimpC a
c)) (forall a. Fixpoint a => a -> Doc
toFix (forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SimpC a
c))

instance Fixpoint a => Fixpoint (WfC a) where
  toFix :: WfC a -> Doc
toFix WfC a
w     = Doc -> BindId -> Doc -> Doc
hang ([Char] -> Doc
text [Char]
"\n\nwf:") BindId
2 Doc
bd
    where bd :: Doc
bd  =   forall a. Fixpoint a => a -> Doc
toFix (forall a. WfC a -> IBindEnv
wenv WfC a
w)
              -- NOTE: this next line is printed this way for compatability with the OCAML solver
              Doc -> Doc -> Doc
$+$ [Char] -> Doc
text [Char]
"reft" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix (Sort -> Reft -> SortedReft
RR Sort
t ((Symbol, Expr) -> Reft
Reft (Symbol
v, KVar -> Subst -> Expr
PKVar KVar
k forall a. Monoid a => a
mempty)))
              Doc -> Doc -> Doc
$+$ Doc -> Doc -> Doc
toFixMeta ([Char] -> Doc
text [Char]
"wf") (forall a. Fixpoint a => a -> Doc
toFix (forall a. WfC a -> a
winfo WfC a
w))
              Doc -> Doc -> Doc
$+$ if forall a. WfC a -> Bool
isGWfc WfC a
w then Doc -> Doc -> Doc
toFixMeta ([Char] -> Doc
text [Char]
"expr") (forall a. Fixpoint a => a -> Doc
toFix (forall a. WfC a -> Expr
wexpr WfC a
w)) else forall a. Monoid a => a
mempty
          (Symbol
v, Sort
t, KVar
k) = forall a. WfC a -> (Symbol, Sort, KVar)
wrft WfC a
w

toFixMeta :: Doc -> Doc -> Doc
toFixMeta :: Doc -> Doc -> Doc
toFixMeta Doc
k Doc
v = [Char] -> Doc
text [Char]
"// META" Doc -> Doc -> Doc
<+> Doc
k Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
":" Doc -> Doc -> Doc
<+> Doc
v

pprId :: Show a => Maybe a -> Doc
pprId :: forall a. Show a => Maybe a -> Doc
pprId (Just a
i)  = Doc
"id" Doc -> Doc -> Doc
<+> forall a. Show a => a -> Doc
tshow a
i
pprId Maybe a
_         = Doc
""

instance PPrint GFixSolution where
  pprintTidy :: Tidy -> GFixSolution -> Doc
pprintTidy Tidy
k (GSol HashMap KVar (Expr, [Expr])
xs) = [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
"\n\n" (Tidy -> (KVar, (Expr, [Expr])) -> Doc
pprintTidyGradual Tidy
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. HashMap k v -> [(k, v)]
M.toList HashMap KVar (Expr, [Expr])
xs)

pprintTidyGradual :: Tidy -> (KVar, (Expr, [Expr])) -> Doc
pprintTidyGradual :: Tidy -> (KVar, (Expr, [Expr])) -> Doc
pprintTidyGradual Tidy
_ (KVar
x, (Expr
e, [Expr]
es)) = KVar -> Doc
ppLocOfKVar KVar
x Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
":=" Doc -> Doc -> Doc
<+> (Doc -> Expr -> Doc
ppNonTauto Doc
" && " Expr
e Doc -> Doc -> Doc
<-> forall a. PPrint a => a -> Doc
pprint [Expr]
es)

ppLocOfKVar :: KVar -> Doc
ppLocOfKVar :: KVar -> Doc
ppLocOfKVar = [Char] -> Doc
textforall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
dropWhile (forall a. Eq a => a -> a -> Bool
/=Char
'(') forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> [Char]
symbolString forall b c a. (b -> c) -> (a -> b) -> a -> c
.KVar -> Symbol
kv

ppNonTauto :: Doc -> Expr -> Doc
ppNonTauto :: Doc -> Expr -> Doc
ppNonTauto Doc
d Expr
e
  | Expr -> Bool
isTautoPred Expr
e = forall a. Monoid a => a
mempty
  | Bool
otherwise     = forall a. PPrint a => a -> Doc
pprint Expr
e Doc -> Doc -> Doc
<-> Doc
d

instance Show   GFixSolution where
  show :: GFixSolution -> [Char]
show = forall a. PPrint a => a -> [Char]
showpp

----------------------------------------------------------------
instance S.Store QualPattern
instance S.Store QualParam
instance S.Store Qualifier
instance S.Store Kuts
instance S.Store HOInfo
instance S.Store GWInfo
instance S.Store GFixSolution
instance (S.Store a) => S.Store (SubC a)
instance (S.Store a) => S.Store (WfC a)
instance (S.Store a) => S.Store (SimpC a)
instance (S.Store (c a), S.Store a) => S.Store (GInfo c a)

instance NFData QualPattern
instance NFData QualParam
instance NFData Qualifier
instance NFData Kuts
instance NFData HOInfo
instance NFData GFixSolution
instance NFData GWInfo

instance (NFData a) => NFData (SubC a)
instance (NFData a) => NFData (WfC a)
instance (NFData a) => NFData (SimpC a)
instance (NFData (c a), NFData a) => NFData (GInfo c a)
instance (NFData a) => NFData (Result a)

instance Hashable Qualifier
instance Hashable QualPattern
instance Hashable QualParam
instance Hashable Equation

instance B.Binary QualPattern
instance B.Binary QualParam
instance B.Binary Qualifier

---------------------------------------------------------------------------
-- | "Smart Constructors" for Constraints ---------------------------------
---------------------------------------------------------------------------

wfC :: (Fixpoint a) => IBindEnv -> SortedReft -> a -> [WfC a]
wfC :: forall a. Fixpoint a => IBindEnv -> SortedReft -> a -> [WfC a]
wfC IBindEnv
be SortedReft
sr a
x = if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Subst -> Bool
isEmptySubst [Subst]
sus -- ++ gsus)
                 -- NV TO RJ This tests fails with [LT:=GHC.Types.LT][EQ:=GHC.Types.EQ][GT:=GHC.Types.GT]]
                 -- NV TO RJ looks like a resolution issue
                then [forall a. IBindEnv -> (Symbol, Sort, KVar) -> a -> WfC a
WfC IBindEnv
be (Symbol
v, SortedReft -> Sort
sr_sort SortedReft
sr, KVar
k) a
x      | KVar
k         <- [KVar]
ks ]
                  forall a. [a] -> [a] -> [a]
++ [forall a.
IBindEnv -> (Symbol, Sort, KVar) -> a -> Expr -> GradInfo -> WfC a
GWfC IBindEnv
be (Symbol
v, SortedReft -> Sort
sr_sort SortedReft
sr, KVar
k) a
x Expr
e GradInfo
i | (KVar
k, Expr
e, GradInfo
i) <- [(KVar, Expr, GradInfo)]
gs ]
                else forall a. (?callStack::CallStack) => [Char] -> a
errorstar [Char]
msg
  where
    msg :: [Char]
msg             = [Char]
"wfKvar: malformed wfC " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show SortedReft
sr forall a. [a] -> [a] -> [a]
++ [Char]
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ([Subst]
sus forall a. [a] -> [a] -> [a]
++ [Subst]
gsus)
    Reft (Symbol
v, Expr
ras)   = SortedReft -> Reft
sr_reft SortedReft
sr
    ([KVar]
ks, [Subst]
sus)       = forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ Expr -> [(KVar, Subst)]
go Expr
ras
    ([(KVar, Expr, GradInfo)]
gs, [Subst]
gsus)      = forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ Expr -> [((KVar, Expr, GradInfo), Subst)]
go' Expr
ras

    go :: Expr -> [(KVar, Subst)]
go (PKVar KVar
k Subst
su) = [(KVar
k, Subst
su)]
    go (PAnd [Expr]
es)    = [(KVar
k, Subst
su) | PKVar KVar
k Subst
su <- [Expr]
es]
    go Expr
_            = []

    go' :: Expr -> [((KVar, Expr, GradInfo), Subst)]
go' (PGrad KVar
k Subst
su GradInfo
i Expr
e) = [((KVar
k, Expr
e, GradInfo
i), Subst
su)]
    go' (PAnd [Expr]
es)      = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [((KVar, Expr, GradInfo), Subst)]
go' [Expr]
es
    go' Expr
_              = []

mkSubC :: IBindEnv -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a
mkSubC :: forall a.
IBindEnv
-> SortedReft
-> SortedReft
-> Maybe SubcId
-> [BindId]
-> a
-> SubC a
mkSubC = forall a.
IBindEnv
-> SortedReft
-> SortedReft
-> Maybe SubcId
-> [BindId]
-> a
-> SubC a
SubC

subC :: IBindEnv -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> [SubC a]
subC :: forall a.
IBindEnv
-> SortedReft
-> SortedReft
-> Maybe SubcId
-> [BindId]
-> a
-> [SubC a]
subC IBindEnv
γ SortedReft
sr1 SortedReft
sr2 Maybe SubcId
i [BindId]
y a
z = [forall a.
IBindEnv
-> SortedReft
-> SortedReft
-> Maybe SubcId
-> [BindId]
-> a
-> SubC a
SubC IBindEnv
γ SortedReft
sr1' (Reft -> SortedReft
sr2' Reft
r2') Maybe SubcId
i [BindId]
y a
z | Reft
r2' <- Reft -> [Reft]
reftConjuncts Reft
r2]
   where
     RR Sort
t1 Reft
r1          = SortedReft
sr1
     RR Sort
t2 Reft
r2          = SortedReft
sr2
     sr1' :: SortedReft
sr1'              = Sort -> Reft -> SortedReft
RR Sort
t1 forall a b. (a -> b) -> a -> b
$ Reft -> Symbol -> Reft
shiftVV Reft
r1  Symbol
vv'
     sr2' :: Reft -> SortedReft
sr2' Reft
r2'          = Sort -> Reft -> SortedReft
RR Sort
t2 forall a b. (a -> b) -> a -> b
$ Reft -> Symbol -> Reft
shiftVV Reft
r2' Symbol
vv'
     vv' :: Symbol
vv'               = Maybe SubcId -> Symbol
mkVV Maybe SubcId
i

mkVV :: Maybe Integer -> Symbol
mkVV :: Maybe SubcId -> Symbol
mkVV (Just SubcId
i)  = Maybe SubcId -> Symbol
vv forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just SubcId
i
mkVV Maybe SubcId
Nothing   = Symbol
vvCon

shiftVV :: Reft -> Symbol -> Reft
shiftVV :: Reft -> Symbol -> Reft
shiftVV r :: Reft
r@(Reft (Symbol
v, Expr
ras)) Symbol
v'
   | Symbol
v forall a. Eq a => a -> a -> Bool
== Symbol
v'   = Reft
r
   | Bool
otherwise = (Symbol, Expr) -> Reft
Reft (Symbol
v', forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 Expr
ras (Symbol
v, Symbol -> Expr
EVar Symbol
v'))

addIds :: [SubC a] -> [(Integer, SubC a)]
addIds :: forall a. [SubC a] -> [(SubcId, SubC a)]
addIds = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\SubcId
i SubC a
c -> (SubcId
i, forall {a} {a}. Show a => a -> SubC a -> SubC a
shiftId SubcId
i forall a b. (a -> b) -> a -> b
$ SubC a
c {_sid :: Maybe SubcId
_sid = forall a. a -> Maybe a
Just SubcId
i})) [SubcId
1..]
  where
    -- Adding shiftId to have distinct VV for SMT conversion
    shiftId :: a -> SubC a -> SubC a
shiftId a
i SubC a
c = SubC a
c { slhs :: SortedReft
slhs = forall {a}. Show a => a -> SortedReft -> SortedReft
shiftSR a
i (forall a. SubC a -> SortedReft
slhs SubC a
c) }
                    { srhs :: SortedReft
srhs = forall {a}. Show a => a -> SortedReft -> SortedReft
shiftSR a
i (forall a. SubC a -> SortedReft
srhs SubC a
c) }
    shiftSR :: a -> SortedReft -> SortedReft
shiftSR a
i SortedReft
sr = SortedReft
sr { sr_reft :: Reft
sr_reft = forall {a}. Show a => a -> Reft -> Reft
shiftR a
i forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft SortedReft
sr }
    shiftR :: a -> Reft -> Reft
shiftR a
i r :: Reft
r@(Reft (Symbol
v, Expr
_)) = Reft -> Symbol -> Reft
shiftVV Reft
r (forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
v a
i)

--------------------------------------------------------------------------------
-- | Qualifiers ----------------------------------------------------------------
--------------------------------------------------------------------------------
data Qualifier = Q
  { Qualifier -> Symbol
qName   :: !Symbol     -- ^ Name
  , Qualifier -> [QualParam]
qParams :: [QualParam] -- ^ Parameters
  , Qualifier -> Expr
qBody   :: !Expr       -- ^ Predicate
  , Qualifier -> SourcePos
qPos    :: !SourcePos  -- ^ Source Location
  }
  deriving (Qualifier -> Qualifier -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Qualifier -> Qualifier -> Bool
$c/= :: Qualifier -> Qualifier -> Bool
== :: Qualifier -> Qualifier -> Bool
$c== :: Qualifier -> Qualifier -> Bool
Eq, Eq Qualifier
Qualifier -> Qualifier -> Bool
Qualifier -> Qualifier -> Ordering
Qualifier -> Qualifier -> Qualifier
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Qualifier -> Qualifier -> Qualifier
$cmin :: Qualifier -> Qualifier -> Qualifier
max :: Qualifier -> Qualifier -> Qualifier
$cmax :: Qualifier -> Qualifier -> Qualifier
>= :: Qualifier -> Qualifier -> Bool
$c>= :: Qualifier -> Qualifier -> Bool
> :: Qualifier -> Qualifier -> Bool
$c> :: Qualifier -> Qualifier -> Bool
<= :: Qualifier -> Qualifier -> Bool
$c<= :: Qualifier -> Qualifier -> Bool
< :: Qualifier -> Qualifier -> Bool
$c< :: Qualifier -> Qualifier -> Bool
compare :: Qualifier -> Qualifier -> Ordering
$ccompare :: Qualifier -> Qualifier -> Ordering
Ord, BindId -> Qualifier -> ShowS
[Qualifier] -> ShowS
Qualifier -> [Char]
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Qualifier] -> ShowS
$cshowList :: [Qualifier] -> ShowS
show :: Qualifier -> [Char]
$cshow :: Qualifier -> [Char]
showsPrec :: BindId -> Qualifier -> ShowS
$cshowsPrec :: BindId -> Qualifier -> ShowS
Show, Typeable Qualifier
Qualifier -> DataType
Qualifier -> Constr
(forall b. Data b => b -> b) -> Qualifier -> Qualifier
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. BindId -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. BindId -> (forall d. Data d => d -> u) -> Qualifier -> u
forall u. (forall d. Data d => d -> u) -> Qualifier -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Qualifier
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Qualifier -> c Qualifier
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Qualifier)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Qualifier)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
gmapQi :: forall u. BindId -> (forall d. Data d => d -> u) -> Qualifier -> u
$cgmapQi :: forall u. BindId -> (forall d. Data d => d -> u) -> Qualifier -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Qualifier -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Qualifier -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
gmapT :: (forall b. Data b => b -> b) -> Qualifier -> Qualifier
$cgmapT :: (forall b. Data b => b -> b) -> Qualifier -> Qualifier
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Qualifier)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Qualifier)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Qualifier)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Qualifier)
dataTypeOf :: Qualifier -> DataType
$cdataTypeOf :: Qualifier -> DataType
toConstr :: Qualifier -> Constr
$ctoConstr :: Qualifier -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Qualifier
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Qualifier
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Qualifier -> c Qualifier
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Qualifier -> c Qualifier
Data, Typeable, forall x. Rep Qualifier x -> Qualifier
forall x. Qualifier -> Rep Qualifier x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Qualifier x -> Qualifier
$cfrom :: forall x. Qualifier -> Rep Qualifier x
Generic)

data QualParam = QP
  { QualParam -> Symbol
qpSym  :: !Symbol
  , QualParam -> QualPattern
qpPat  :: !QualPattern
  , QualParam -> Sort
qpSort :: !Sort
  }
  deriving (QualParam -> QualParam -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: QualParam -> QualParam -> Bool
$c/= :: QualParam -> QualParam -> Bool
== :: QualParam -> QualParam -> Bool
$c== :: QualParam -> QualParam -> Bool
Eq, Eq QualParam
QualParam -> QualParam -> Bool
QualParam -> QualParam -> Ordering
QualParam -> QualParam -> QualParam
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: QualParam -> QualParam -> QualParam
$cmin :: QualParam -> QualParam -> QualParam
max :: QualParam -> QualParam -> QualParam
$cmax :: QualParam -> QualParam -> QualParam
>= :: QualParam -> QualParam -> Bool
$c>= :: QualParam -> QualParam -> Bool
> :: QualParam -> QualParam -> Bool
$c> :: QualParam -> QualParam -> Bool
<= :: QualParam -> QualParam -> Bool
$c<= :: QualParam -> QualParam -> Bool
< :: QualParam -> QualParam -> Bool
$c< :: QualParam -> QualParam -> Bool
compare :: QualParam -> QualParam -> Ordering
$ccompare :: QualParam -> QualParam -> Ordering
Ord, BindId -> QualParam -> ShowS
[QualParam] -> ShowS
QualParam -> [Char]
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [QualParam] -> ShowS
$cshowList :: [QualParam] -> ShowS
show :: QualParam -> [Char]
$cshow :: QualParam -> [Char]
showsPrec :: BindId -> QualParam -> ShowS
$cshowsPrec :: BindId -> QualParam -> ShowS
Show, Typeable QualParam
QualParam -> DataType
QualParam -> Constr
(forall b. Data b => b -> b) -> QualParam -> QualParam
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. BindId -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. BindId -> (forall d. Data d => d -> u) -> QualParam -> u
forall u. (forall d. Data d => d -> u) -> QualParam -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualParam -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualParam -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QualParam
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualParam -> c QualParam
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QualParam)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QualParam)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam
gmapQi :: forall u. BindId -> (forall d. Data d => d -> u) -> QualParam -> u
$cgmapQi :: forall u. BindId -> (forall d. Data d => d -> u) -> QualParam -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> QualParam -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> QualParam -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualParam -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualParam -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualParam -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualParam -> r
gmapT :: (forall b. Data b => b -> b) -> QualParam -> QualParam
$cgmapT :: (forall b. Data b => b -> b) -> QualParam -> QualParam
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QualParam)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QualParam)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QualParam)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QualParam)
dataTypeOf :: QualParam -> DataType
$cdataTypeOf :: QualParam -> DataType
toConstr :: QualParam -> Constr
$ctoConstr :: QualParam -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QualParam
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QualParam
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualParam -> c QualParam
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualParam -> c QualParam
Data, Typeable, forall x. Rep QualParam x -> QualParam
forall x. QualParam -> Rep QualParam x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep QualParam x -> QualParam
$cfrom :: forall x. QualParam -> Rep QualParam x
Generic)

data QualPattern
  = PatNone                 -- ^ match everything
  | PatPrefix !Symbol !Int  -- ^ str . $i  i.e. match prefix 'str' with suffix bound to $i
  | PatSuffix !Int !Symbol  -- ^ $i . str  i.e. match suffix 'str' with prefix bound to $i
  | PatExact  !Symbol       -- ^ str       i.e. exactly match 'str'
  deriving (QualPattern -> QualPattern -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: QualPattern -> QualPattern -> Bool
$c/= :: QualPattern -> QualPattern -> Bool
== :: QualPattern -> QualPattern -> Bool
$c== :: QualPattern -> QualPattern -> Bool
Eq, Eq QualPattern
QualPattern -> QualPattern -> Bool
QualPattern -> QualPattern -> Ordering
QualPattern -> QualPattern -> QualPattern
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: QualPattern -> QualPattern -> QualPattern
$cmin :: QualPattern -> QualPattern -> QualPattern
max :: QualPattern -> QualPattern -> QualPattern
$cmax :: QualPattern -> QualPattern -> QualPattern
>= :: QualPattern -> QualPattern -> Bool
$c>= :: QualPattern -> QualPattern -> Bool
> :: QualPattern -> QualPattern -> Bool
$c> :: QualPattern -> QualPattern -> Bool
<= :: QualPattern -> QualPattern -> Bool
$c<= :: QualPattern -> QualPattern -> Bool
< :: QualPattern -> QualPattern -> Bool
$c< :: QualPattern -> QualPattern -> Bool
compare :: QualPattern -> QualPattern -> Ordering
$ccompare :: QualPattern -> QualPattern -> Ordering
Ord, BindId -> QualPattern -> ShowS
[QualPattern] -> ShowS
QualPattern -> [Char]
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [QualPattern] -> ShowS
$cshowList :: [QualPattern] -> ShowS
show :: QualPattern -> [Char]
$cshow :: QualPattern -> [Char]
showsPrec :: BindId -> QualPattern -> ShowS
$cshowsPrec :: BindId -> QualPattern -> ShowS
Show, Typeable QualPattern
QualPattern -> DataType
QualPattern -> Constr
(forall b. Data b => b -> b) -> QualPattern -> QualPattern
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. BindId -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
BindId -> (forall d. Data d => d -> u) -> QualPattern -> u
forall u. (forall d. Data d => d -> u) -> QualPattern -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualPattern -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualPattern -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QualPattern
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualPattern -> c QualPattern
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QualPattern)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c QualPattern)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
gmapQi :: forall u.
BindId -> (forall d. Data d => d -> u) -> QualPattern -> u
$cgmapQi :: forall u.
BindId -> (forall d. Data d => d -> u) -> QualPattern -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> QualPattern -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> QualPattern -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualPattern -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualPattern -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualPattern -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualPattern -> r
gmapT :: (forall b. Data b => b -> b) -> QualPattern -> QualPattern
$cgmapT :: (forall b. Data b => b -> b) -> QualPattern -> QualPattern
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c QualPattern)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c QualPattern)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QualPattern)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QualPattern)
dataTypeOf :: QualPattern -> DataType
$cdataTypeOf :: QualPattern -> DataType
toConstr :: QualPattern -> Constr
$ctoConstr :: QualPattern -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QualPattern
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QualPattern
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualPattern -> c QualPattern
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualPattern -> c QualPattern
Data, Typeable, forall x. Rep QualPattern x -> QualPattern
forall x. QualPattern -> Rep QualPattern x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep QualPattern x -> QualPattern
$cfrom :: forall x. QualPattern -> Rep QualPattern x
Generic)

trueQual :: Qualifier
trueQual :: Qualifier
trueQual = Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
Q (forall a. Symbolic a => a -> Symbol
symbol ([Char]
"QTrue" :: String)) [] forall a. Monoid a => a
mempty ([Char] -> SourcePos
dummyPos [Char]
"trueQual")

instance Loc Qualifier where
  srcSpan :: Qualifier -> SrcSpan
srcSpan Qualifier
q = SourcePos -> SourcePos -> SrcSpan
SS SourcePos
l SourcePos
l
    where
      l :: SourcePos
l     = Qualifier -> SourcePos
qPos Qualifier
q

instance Subable Qualifier where
  syms :: Qualifier -> [Symbol]
syms   = Qualifier -> [Symbol]
qualFreeSymbols
  subst :: Subst -> Qualifier -> Qualifier
subst  = (Expr -> Expr) -> Qualifier -> Qualifier
mapQualBody forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subable a => Subst -> a -> a
subst
  substf :: (Symbol -> Expr) -> Qualifier -> Qualifier
substf = (Expr -> Expr) -> Qualifier -> Qualifier
mapQualBody forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subable a => (Symbol -> Expr) -> a -> a
substf
  substa :: (Symbol -> Symbol) -> Qualifier -> Qualifier
substa = (Expr -> Expr) -> Qualifier -> Qualifier
mapQualBody forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa

mapQualBody :: (Expr -> Expr) -> Qualifier -> Qualifier
mapQualBody :: (Expr -> Expr) -> Qualifier -> Qualifier
mapQualBody Expr -> Expr
f Qualifier
q = Qualifier
q { qBody :: Expr
qBody = Expr -> Expr
f (Qualifier -> Expr
qBody Qualifier
q) }

qualFreeSymbols :: Qualifier -> [Symbol]
qualFreeSymbols :: Qualifier -> [Symbol]
qualFreeSymbols Qualifier
q = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Bool
isPrim) [Symbol]
xs
  where
    xs :: [Symbol]
xs            = forall a. Subable a => a -> [Symbol]
syms (Qualifier -> Expr
qBody Qualifier
q) forall a. Eq a => [a] -> [a] -> [a]
L.\\ forall a. Subable a => a -> [Symbol]
syms (QualParam -> Symbol
qpSym forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Qualifier -> [QualParam]
qParams Qualifier
q)

instance Fixpoint QualParam where
  toFix :: QualParam -> Doc
toFix (QP Symbol
x QualPattern
_ Sort
t) = forall a. Fixpoint a => a -> Doc
toFix (Symbol
x, Sort
t)

instance PPrint QualParam where
  pprintTidy :: Tidy -> QualParam -> Doc
pprintTidy Tidy
k (QP Symbol
x QualPattern
pat Sort
t) = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
x Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k QualPattern
pat Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Sort
t

instance PPrint QualPattern where
  pprintTidy :: Tidy -> QualPattern -> Doc
pprintTidy Tidy
_ QualPattern
PatNone         = Doc
""
  pprintTidy Tidy
k (PatPrefix Symbol
s BindId
i) = Doc
"as" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
s Doc -> Doc -> Doc
<+> (Doc
"$" Doc -> Doc -> Doc
<-> forall a. PPrint a => a -> Doc
pprint BindId
i)
  pprintTidy Tidy
k (PatSuffix BindId
s Symbol
i) = Doc
"as" Doc -> Doc -> Doc
<+> (Doc
"$" Doc -> Doc -> Doc
<-> forall a. PPrint a => a -> Doc
pprint Symbol
i) Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k BindId
s
  pprintTidy Tidy
k (PatExact  Symbol
s  ) = Doc
"~"  Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
s

instance Fixpoint Qualifier where
  toFix :: Qualifier -> Doc
toFix = Qualifier -> Doc
pprQual

instance PPrint Qualifier where
  pprintTidy :: Tidy -> Qualifier -> Doc
pprintTidy Tidy
k Qualifier
q = Doc
"qualif" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Qualifier -> Symbol
qName Qualifier
q) Doc -> Doc -> Doc
<+> Doc
"defined at" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Qualifier -> SourcePos
qPos Qualifier
q)
  -- pprintTidy _ q = pprQual q

pprQual :: Qualifier -> Doc
pprQual :: Qualifier -> Doc
pprQual (Q Symbol
n [QualParam]
xts Expr
p SourcePos
l) = [Char] -> Doc
text [Char]
"qualif" Doc -> Doc -> Doc
<+> [Char] -> Doc
text (Symbol -> [Char]
symbolString Symbol
n) Doc -> Doc -> Doc
<-> Doc -> Doc
parens Doc
args Doc -> Doc -> Doc
<-> Doc
colon Doc -> Doc -> Doc
<+> Doc -> Doc
parens (forall a. Fixpoint a => a -> Doc
toFix Expr
p) Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"//" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix SourcePos
l
  where
    args :: Doc
args              = Doc -> [Doc] -> Doc
intersperse Doc
comma (forall a. Fixpoint a => a -> Doc
toFix forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [QualParam]
xts)

qualifier :: SEnv Sort -> SourcePos -> SEnv Sort -> Symbol -> Sort -> Expr -> Qualifier
qualifier :: SEnv Sort
-> SourcePos -> SEnv Sort -> Symbol -> Sort -> Expr -> Qualifier
qualifier SEnv Sort
lEnv SourcePos
l SEnv Sort
γ Symbol
v Sort
so Expr
p   = Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier
mkQ Symbol
"Auto" ((Symbol
v, Sort
so) forall a. a -> [a] -> [a]
: [(Symbol, Sort)]
xts) Expr
p SourcePos
l
  where
    xs :: [Symbol]
xs  = forall a. Eq a => a -> [a] -> [a]
L.delete Symbol
v forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a]
L.nub forall a b. (a -> b) -> a -> b
$ forall a. Subable a => a -> [Symbol]
syms Expr
p
    xts :: [(Symbol, Sort)]
xts = forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (SourcePos
-> SEnv Sort
-> SEnv Sort
-> Symbol
-> SubcId
-> Maybe (Symbol, Sort)
envSort SourcePos
l SEnv Sort
lEnv SEnv Sort
γ) [Symbol]
xs [SubcId
0..]

mkQ :: Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier
mkQ :: Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier
mkQ Symbol
n = Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
Q Symbol
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, Sort)] -> [QualParam]
qualParams

qualParams :: [(Symbol, Sort)] -> [QualParam]
qualParams :: [(Symbol, Sort)] -> [QualParam]
qualParams [(Symbol, Sort)]
xts = [ Symbol -> QualPattern -> Sort -> QualParam
QP Symbol
x QualPattern
PatNone Sort
t | (Symbol
x, Sort
t) <- [(Symbol, Sort)]
xts]

qualBinds   :: Qualifier -> [(Symbol, Sort)]
qualBinds :: Qualifier -> [(Symbol, Sort)]
qualBinds Qualifier
q = [ (QualParam -> Symbol
qpSym QualParam
qp, QualParam -> Sort
qpSort QualParam
qp) | QualParam
qp <- Qualifier -> [QualParam]
qParams Qualifier
q ]

envSort :: SourcePos -> SEnv Sort -> SEnv Sort -> Symbol -> Integer -> Maybe (Symbol, Sort)
envSort :: SourcePos
-> SEnv Sort
-> SEnv Sort
-> Symbol
-> SubcId
-> Maybe (Symbol, Sort)
envSort SourcePos
l SEnv Sort
lEnv SEnv Sort
tEnv Symbol
x SubcId
i
  | Just Sort
t <- forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
x SEnv Sort
tEnv = forall a. a -> Maybe a
Just (Symbol
x, Sort
t)
  | Just Sort
_ <- forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
x SEnv Sort
lEnv = forall a. Maybe a
Nothing
  | Bool
otherwise                   = forall a. a -> Maybe a
Just (Symbol
x, Sort
ai)
  where
    ai :: Sort
ai  = {- trace msg $ -} LocSymbol -> Sort
fObj forall a b. (a -> b) -> a -> b
$ forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l forall a b. (a -> b) -> a -> b
$ Symbol -> SubcId -> Symbol
tempSymbol Symbol
"LHTV" SubcId
i
    -- msg = "unknown symbol in qualifier: " ++ show x

remakeQual :: Qualifier -> Qualifier
remakeQual :: Qualifier -> Qualifier
remakeQual Qualifier
q = Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
mkQual (Qualifier -> Symbol
qName Qualifier
q) (Qualifier -> [QualParam]
qParams Qualifier
q) (Qualifier -> Expr
qBody Qualifier
q) (Qualifier -> SourcePos
qPos Qualifier
q)

-- | constructing qualifiers
mkQual :: Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
mkQual :: Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
mkQual Symbol
n [QualParam]
qps Expr
p = Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
Q Symbol
n [QualParam]
qps' Expr
p
  where
    qps' :: [QualParam]
qps'       = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\QualParam
qp Sort
t' -> QualParam
qp { qpSort :: Sort
qpSort = Sort
t'}) [QualParam]
qps [Sort]
ts'
    ts' :: [Sort]
ts'        = [Sort] -> [Sort]
gSorts (QualParam -> Sort
qpSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [QualParam]
qps)

gSorts :: [Sort] -> [Sort]
gSorts :: [Sort] -> [Sort]
gSorts [Sort]
ts = [(Symbol, BindId)] -> Sort -> Sort
substVars [(Symbol, BindId)]
su forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
ts
  where
    su :: [(Symbol, BindId)]
su    = (forall a b. [a] -> [b] -> [(a, b)]
`zip` [BindId
0..]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
sortNub forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Sort -> [Symbol]
sortVars forall a b. (a -> b) -> a -> b
$ [Sort]
ts

substVars :: [(Symbol, Int)] -> Sort -> Sort
substVars :: [(Symbol, BindId)] -> Sort -> Sort
substVars [(Symbol, BindId)]
su = (Sort -> Sort) -> Sort -> Sort
mapSort' Sort -> Sort
tx
  where
    tx :: Sort -> Sort
tx (FObj Symbol
x)
      | Just BindId
i <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Symbol
x [(Symbol, BindId)]
su = BindId -> Sort
FVar BindId
i
    tx Sort
t                      = Sort
t

sortVars :: Sort -> [Symbol]
sortVars :: Sort -> [Symbol]
sortVars = forall a. (a -> Sort -> a) -> a -> Sort -> a
foldSort' [Symbol] -> Sort -> [Symbol]
go []
  where
    go :: [Symbol] -> Sort -> [Symbol]
go [Symbol]
b (FObj Symbol
x) = Symbol
x forall a. a -> [a] -> [a]
: [Symbol]
b
    go [Symbol]
b Sort
_        = [Symbol]
b

-- COPIED from Visitor due to cyclic deps
mapSort' :: (Sort -> Sort) -> Sort -> Sort
mapSort' :: (Sort -> Sort) -> Sort -> Sort
mapSort' Sort -> Sort
f = Sort -> Sort
step
  where
    step :: Sort -> Sort
step             = Sort -> Sort
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Sort
f
    go :: Sort -> Sort
go (FFunc Sort
t1 Sort
t2) = Sort -> Sort -> Sort
FFunc (Sort -> Sort
step Sort
t1) (Sort -> Sort
step Sort
t2)
    go (FApp Sort
t1 Sort
t2)  = Sort -> Sort -> Sort
FApp (Sort -> Sort
step Sort
t1) (Sort -> Sort
step Sort
t2)
    go (FAbs BindId
i Sort
t)    = BindId -> Sort -> Sort
FAbs BindId
i (Sort -> Sort
step Sort
t)
    go Sort
t             = Sort
t

-- COPIED from Visitor due to cyclic deps
foldSort' :: (a -> Sort -> a) -> a -> Sort -> a
foldSort' :: forall a. (a -> Sort -> a) -> a -> Sort -> a
foldSort' a -> Sort -> a
f = a -> Sort -> a
step
  where
    step :: a -> Sort -> a
step a
b Sort
t           = a -> Sort -> a
go (a -> Sort -> a
f a
b Sort
t) Sort
t
    go :: a -> Sort -> a
go a
b (FFunc Sort
t1 Sort
t2) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' a -> Sort -> a
step a
b [Sort
t1, Sort
t2]
    go a
b (FApp Sort
t1 Sort
t2)  = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' a -> Sort -> a
step a
b [Sort
t1, Sort
t2]
    go a
b (FAbs BindId
_ Sort
t)    = a -> Sort -> a
go a
b Sort
t
    go a
b Sort
_             = a
b


--------------------------------------------------------------------------------
-- | Constraint Cut Sets -------------------------------------------------------
--------------------------------------------------------------------------------

newtype Kuts = KS { Kuts -> HashSet KVar
ksVars :: S.HashSet KVar }
               deriving (Kuts -> Kuts -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Kuts -> Kuts -> Bool
$c/= :: Kuts -> Kuts -> Bool
== :: Kuts -> Kuts -> Bool
$c== :: Kuts -> Kuts -> Bool
Eq, BindId -> Kuts -> ShowS
[Kuts] -> ShowS
Kuts -> [Char]
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Kuts] -> ShowS
$cshowList :: [Kuts] -> ShowS
show :: Kuts -> [Char]
$cshow :: Kuts -> [Char]
showsPrec :: BindId -> Kuts -> ShowS
$cshowsPrec :: BindId -> Kuts -> ShowS
Show, forall x. Rep Kuts x -> Kuts
forall x. Kuts -> Rep Kuts x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Kuts x -> Kuts
$cfrom :: forall x. Kuts -> Rep Kuts x
Generic)

instance Fixpoint Kuts where
  toFix :: Kuts -> Doc
toFix (KS HashSet KVar
s) = [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ (Doc
"cut " Doc -> Doc -> Doc
<->) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fixpoint a => a -> Doc
toFix forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Ord a => [a] -> [a]
L.sort (forall a. HashSet a -> [a]
S.toList HashSet KVar
s)

ksMember :: KVar -> Kuts -> Bool
ksMember :: KVar -> Kuts -> Bool
ksMember KVar
k (KS HashSet KVar
s) = forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member KVar
k HashSet KVar
s

instance Semigroup Kuts where
  Kuts
k1 <> :: Kuts -> Kuts -> Kuts
<> Kuts
k2 = HashSet KVar -> Kuts
KS forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union (Kuts -> HashSet KVar
ksVars Kuts
k1) (Kuts -> HashSet KVar
ksVars Kuts
k2)

instance Monoid Kuts where
  mempty :: Kuts
mempty  = HashSet KVar -> Kuts
KS forall a. HashSet a
S.empty
  mappend :: Kuts -> Kuts -> Kuts
mappend = forall a. Semigroup a => a -> a -> a
(<>)

------------------------------------------------------------------------
-- | Constructing Queries
------------------------------------------------------------------------
fi :: [SubC a]
   -> [WfC a]
   -> BindEnv a
   -> SEnv Sort
   -> SEnv Sort
   -> Kuts
   -> [Qualifier]
   -> M.HashMap BindId a
   -> Bool
   -> Bool
   -> [Triggered Expr]
   -> AxiomEnv
   -> [DataDecl]
   -> [BindId]
   -> GInfo SubC a
fi :: forall a.
[SubC a]
-> [WfC a]
-> BindEnv a
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap BindId a
-> Bool
-> Bool
-> [Triggered Expr]
-> AxiomEnv
-> [DataDecl]
-> [BindId]
-> GInfo SubC a
fi [SubC a]
cs [WfC a]
ws BindEnv a
binds SEnv Sort
ls SEnv Sort
ds Kuts
ks [Qualifier]
qs HashMap BindId a
bi Bool
aHO Bool
aHOq [Triggered Expr]
es AxiomEnv
axe [DataDecl]
adts [BindId]
ebs
  = FI { cm :: HashMap SubcId (SubC a)
cm       = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ forall a. [SubC a] -> [(SubcId, SubC a)]
addIds [SubC a]
cs
       , ws :: HashMap KVar (WfC a)
ws       = forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> [(k, v)] -> HashMap k v
M.fromListWith forall {a}. a
err [(KVar
k, WfC a
w) | WfC a
w <- [WfC a]
ws, let (Symbol
_, Sort
_, KVar
k) = forall a. WfC a -> (Symbol, Sort, KVar)
wrft WfC a
w]
       , bs :: BindEnv a
bs       = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a.
((Symbol, SortedReft) -> (Symbol, SortedReft))
-> BindId -> BindEnv a -> BindEnv a
adjustBindEnv forall {a}. (a, SortedReft) -> (a, SortedReft)
stripReft) BindEnv a
binds [BindId]
ebs
       , gLits :: SEnv Sort
gLits    = SEnv Sort
ls
       , dLits :: SEnv Sort
dLits    = SEnv Sort
ds
       , kuts :: Kuts
kuts     = Kuts
ks
       , quals :: [Qualifier]
quals    = [Qualifier]
qs
       , bindInfo :: HashMap BindId a
bindInfo = HashMap BindId a
bi
       , hoInfo :: HOInfo
hoInfo   = Bool -> Bool -> HOInfo
HOI Bool
aHO Bool
aHOq
       , asserts :: [Triggered Expr]
asserts  = [Triggered Expr]
es
       , ae :: AxiomEnv
ae       = AxiomEnv
axe
       , ddecls :: [DataDecl]
ddecls   = [DataDecl]
adts
       , ebinds :: [BindId]
ebinds   = [BindId]
ebs
       }
  where
    --TODO handle duplicates gracefully instead (merge envs by intersect?)
    err :: a
err = forall a. (?callStack::CallStack) => [Char] -> a
errorstar [Char]
"multiple WfCs with same kvar"
    stripReft :: (a, SortedReft) -> (a, SortedReft)
stripReft (a
sym, SortedReft
reft) = (a
sym, SortedReft
reft { sr_reft :: Reft
sr_reft = Reft
trueReft })

------------------------------------------------------------------------
-- | Top-level Queries
------------------------------------------------------------------------

data FInfoWithOpts a = FIO
  { forall a. FInfoWithOpts a -> FInfo a
fioFI   :: FInfo a
  , forall a. FInfoWithOpts a -> [[Char]]
fioOpts :: [String]
  }

type FInfo a   = GInfo SubC a
type SInfo a   = GInfo SimpC a

data HOInfo = HOI
  { HOInfo -> Bool
hoBinds :: Bool          -- ^ Allow higher order binds in the environemnt
  , HOInfo -> Bool
hoQuals :: Bool          -- ^ Allow higher order quals
  }
  deriving (HOInfo -> HOInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HOInfo -> HOInfo -> Bool
$c/= :: HOInfo -> HOInfo -> Bool
== :: HOInfo -> HOInfo -> Bool
$c== :: HOInfo -> HOInfo -> Bool
Eq, BindId -> HOInfo -> ShowS
[HOInfo] -> ShowS
HOInfo -> [Char]
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [HOInfo] -> ShowS
$cshowList :: [HOInfo] -> ShowS
show :: HOInfo -> [Char]
$cshow :: HOInfo -> [Char]
showsPrec :: BindId -> HOInfo -> ShowS
$cshowsPrec :: BindId -> HOInfo -> ShowS
Show, forall x. Rep HOInfo x -> HOInfo
forall x. HOInfo -> Rep HOInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep HOInfo x -> HOInfo
$cfrom :: forall x. HOInfo -> Rep HOInfo x
Generic)

allowHO, allowHOquals :: GInfo c a -> Bool
allowHO :: forall (c :: * -> *) a. GInfo c a -> Bool
allowHO      = HOInfo -> Bool
hoBinds forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> HOInfo
hoInfo
allowHOquals :: forall (c :: * -> *) a. GInfo c a -> Bool
allowHOquals = HOInfo -> Bool
hoQuals forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> HOInfo
hoInfo

data GInfo c a = FI
  { forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm       :: !(M.HashMap SubcId (c a))  -- ^ cst id |-> Horn Constraint
  , forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws       :: !(M.HashMap KVar (WfC a))  -- ^ Kvar  |-> WfC defining its scope/args
  , forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs       :: !(BindEnv a)               -- ^ Bind  |-> (Symbol, SortedReft)
  , forall (c :: * -> *) a. GInfo c a -> [BindId]
ebinds   :: ![BindId]                  -- ^ Subset of existential binders
  , forall (c :: * -> *) a. GInfo c a -> SEnv Sort
gLits    :: !(SEnv Sort)               -- ^ Global Constant symbols
  , forall (c :: * -> *) a. GInfo c a -> SEnv Sort
dLits    :: !(SEnv Sort)               -- ^ Distinct Constant symbols
  , forall (c :: * -> *) a. GInfo c a -> Kuts
kuts     :: !Kuts                      -- ^ Set of KVars *not* to eliminate
  , forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals    :: ![Qualifier]               -- ^ Abstract domain
  , forall (c :: * -> *) a. GInfo c a -> HashMap BindId a
bindInfo :: !(M.HashMap BindId a)      -- ^ Metadata about binders
  , forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls   :: ![DataDecl]                -- ^ User-defined data declarations
  , forall (c :: * -> *) a. GInfo c a -> HOInfo
hoInfo   :: !HOInfo                    -- ^ Higher Order info
  , forall (c :: * -> *) a. GInfo c a -> [Triggered Expr]
asserts  :: ![Triggered Expr]          -- ^ TODO: what is this?
  , forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae       :: AxiomEnv                   -- ^ Information about reflected function defs
  }
  deriving (GInfo c a -> GInfo c a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (c :: * -> *) a.
(Eq a, Eq (c a)) =>
GInfo c a -> GInfo c a -> Bool
/= :: GInfo c a -> GInfo c a -> Bool
$c/= :: forall (c :: * -> *) a.
(Eq a, Eq (c a)) =>
GInfo c a -> GInfo c a -> Bool
== :: GInfo c a -> GInfo c a -> Bool
$c== :: forall (c :: * -> *) a.
(Eq a, Eq (c a)) =>
GInfo c a -> GInfo c a -> Bool
Eq, BindId -> GInfo c a -> ShowS
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
BindId -> GInfo c a -> ShowS
forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
[GInfo c a] -> ShowS
forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
GInfo c a -> [Char]
showList :: [GInfo c a] -> ShowS
$cshowList :: forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
[GInfo c a] -> ShowS
show :: GInfo c a -> [Char]
$cshow :: forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
GInfo c a -> [Char]
showsPrec :: BindId -> GInfo c a -> ShowS
$cshowsPrec :: forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
BindId -> GInfo c a -> ShowS
Show, forall a b. a -> GInfo c b -> GInfo c a
forall a b. (a -> b) -> GInfo c a -> GInfo c b
forall (c :: * -> *) a b. Functor c => a -> GInfo c b -> GInfo c a
forall (c :: * -> *) a b.
Functor c =>
(a -> b) -> GInfo c a -> GInfo c 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 -> GInfo c b -> GInfo c a
$c<$ :: forall (c :: * -> *) a b. Functor c => a -> GInfo c b -> GInfo c a
fmap :: forall a b. (a -> b) -> GInfo c a -> GInfo c b
$cfmap :: forall (c :: * -> *) a b.
Functor c =>
(a -> b) -> GInfo c a -> GInfo c b
Functor, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (c :: * -> *) a x. Rep (GInfo c a) x -> GInfo c a
forall (c :: * -> *) a x. GInfo c a -> Rep (GInfo c a) x
$cto :: forall (c :: * -> *) a x. Rep (GInfo c a) x -> GInfo c a
$cfrom :: forall (c :: * -> *) a x. GInfo c a -> Rep (GInfo c a) x
Generic)

instance HasGradual (GInfo c a) where
  isGradual :: GInfo c a -> Bool
isGradual GInfo c a
info = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. HasGradual a => a -> Bool
isGradual (forall k v. HashMap k v -> [v]
M.elems forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws GInfo c a
info)

instance Semigroup HOInfo where
  HOInfo
i1 <> :: HOInfo -> HOInfo -> HOInfo
<> HOInfo
i2 = HOI { hoBinds :: Bool
hoBinds = HOInfo -> Bool
hoBinds HOInfo
i1 Bool -> Bool -> Bool
|| HOInfo -> Bool
hoBinds HOInfo
i2
                 , hoQuals :: Bool
hoQuals = HOInfo -> Bool
hoQuals HOInfo
i1 Bool -> Bool -> Bool
|| HOInfo -> Bool
hoQuals HOInfo
i2
                 }

instance Monoid HOInfo where
  mempty :: HOInfo
mempty        = Bool -> Bool -> HOInfo
HOI Bool
False Bool
False

instance Semigroup (GInfo c a) where
  GInfo c a
i1 <> :: GInfo c a -> GInfo c a -> GInfo c a
<> GInfo c a
i2 = FI { cm :: HashMap SubcId (c a)
cm       = forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm GInfo c a
i1       forall a. Semigroup a => a -> a -> a
<> forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm GInfo c a
i2
                , ws :: HashMap KVar (WfC a)
ws       = forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws GInfo c a
i1       forall a. Semigroup a => a -> a -> a
<> forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws GInfo c a
i2
                , bs :: BindEnv a
bs       = forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs GInfo c a
i1       forall a. Semigroup a => a -> a -> a
<> forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs GInfo c a
i2
                , ebinds :: [BindId]
ebinds   = forall (c :: * -> *) a. GInfo c a -> [BindId]
ebinds GInfo c a
i1   forall a. Semigroup a => a -> a -> a
<> forall (c :: * -> *) a. GInfo c a -> [BindId]
ebinds GInfo c a
i2
                , gLits :: SEnv Sort
gLits    = forall (c :: * -> *) a. GInfo c a -> SEnv Sort
gLits GInfo c a
i1    forall a. Semigroup a => a -> a -> a
<> forall (c :: * -> *) a. GInfo c a -> SEnv Sort
gLits GInfo c a
i2
                , dLits :: SEnv Sort
dLits    = forall (c :: * -> *) a. GInfo c a -> SEnv Sort
dLits GInfo c a
i1    forall a. Semigroup a => a -> a -> a
<> forall (c :: * -> *) a. GInfo c a -> SEnv Sort
dLits GInfo c a
i2
                , kuts :: Kuts
kuts     = forall (c :: * -> *) a. GInfo c a -> Kuts
kuts GInfo c a
i1     forall a. Semigroup a => a -> a -> a
<> forall (c :: * -> *) a. GInfo c a -> Kuts
kuts GInfo c a
i2
                , quals :: [Qualifier]
quals    = forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals GInfo c a
i1    forall a. Semigroup a => a -> a -> a
<> forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals GInfo c a
i2
                , bindInfo :: HashMap BindId a
bindInfo = forall (c :: * -> *) a. GInfo c a -> HashMap BindId a
bindInfo GInfo c a
i1 forall a. Semigroup a => a -> a -> a
<> forall (c :: * -> *) a. GInfo c a -> HashMap BindId a
bindInfo GInfo c a
i2
                , ddecls :: [DataDecl]
ddecls   = forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls GInfo c a
i1   forall a. Semigroup a => a -> a -> a
<> forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls GInfo c a
i2
                , hoInfo :: HOInfo
hoInfo   = forall (c :: * -> *) a. GInfo c a -> HOInfo
hoInfo GInfo c a
i1   forall a. Semigroup a => a -> a -> a
<> forall (c :: * -> *) a. GInfo c a -> HOInfo
hoInfo GInfo c a
i2
                , asserts :: [Triggered Expr]
asserts  = forall (c :: * -> *) a. GInfo c a -> [Triggered Expr]
asserts GInfo c a
i1  forall a. Semigroup a => a -> a -> a
<> forall (c :: * -> *) a. GInfo c a -> [Triggered Expr]
asserts GInfo c a
i2
                , ae :: AxiomEnv
ae       = forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae GInfo c a
i1       forall a. Semigroup a => a -> a -> a
<> forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae GInfo c a
i2
                }


instance Monoid (GInfo c a) where
  mempty :: GInfo c a
mempty        = FI { cm :: HashMap SubcId (c a)
cm       = forall k v. HashMap k v
M.empty
                     , ws :: HashMap KVar (WfC a)
ws       = forall a. Monoid a => a
mempty
                     , bs :: BindEnv a
bs       = forall a. Monoid a => a
mempty
                     , ebinds :: [BindId]
ebinds   = forall a. Monoid a => a
mempty
                     , gLits :: SEnv Sort
gLits    = forall a. Monoid a => a
mempty
                     , dLits :: SEnv Sort
dLits    = forall a. Monoid a => a
mempty
                     , kuts :: Kuts
kuts     = forall a. Monoid a => a
mempty
                     , quals :: [Qualifier]
quals    = forall a. Monoid a => a
mempty
                     , bindInfo :: HashMap BindId a
bindInfo = forall a. Monoid a => a
mempty
                     , ddecls :: [DataDecl]
ddecls   = forall a. Monoid a => a
mempty
                     , hoInfo :: HOInfo
hoInfo   = forall a. Monoid a => a
mempty
                     , asserts :: [Triggered Expr]
asserts  = forall a. Monoid a => a
mempty
                     , ae :: AxiomEnv
ae       = forall a. Monoid a => a
mempty
                     }

instance PTable (SInfo a) where
  ptable :: SInfo a -> DocTable
ptable SInfo a
z = [(Doc, Doc)] -> DocTable
DocTable [ ([Char] -> Doc
text [Char]
"# Sub Constraints", forall a. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> BindId
length forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
z)
                      , ([Char] -> Doc
text [Char]
"# WF  Constraints", forall a. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> BindId
length forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws SInfo a
z)
                      ]

--------------------------------------------------------------------------
-- | Rendering Queries
--------------------------------------------------------------------------
toFixpoint :: (Fixpoint a, Fixpoint (c a)) => Config -> GInfo c a -> Doc
--------------------------------------------------------------------------
toFixpoint :: forall a (c :: * -> *).
(Fixpoint a, Fixpoint (c a)) =>
Config -> GInfo c a -> Doc
toFixpoint Config
cfg GInfo c a
x' =    forall a. Show a => a -> Doc
cfgDoc   Config
cfg
                  Doc -> Doc -> Doc
$++$ forall {c :: * -> *} {a}. GInfo c a -> Doc
declsDoc GInfo c a
x'
                  Doc -> Doc -> Doc
$++$ forall {c :: * -> *} {a}. GInfo c a -> Doc
aeDoc    GInfo c a
x'
                  Doc -> Doc -> Doc
$++$ forall {c :: * -> *} {a}. GInfo c a -> Doc
qualsDoc GInfo c a
x'
                  Doc -> Doc -> Doc
$++$ forall {c :: * -> *} {a}. GInfo c a -> Doc
kutsDoc  GInfo c a
x'
                --   $++$ packsDoc x'
                  Doc -> Doc -> Doc
$++$ forall {c :: * -> *} {a}. GInfo c a -> Doc
gConDoc   GInfo c a
x'
                  Doc -> Doc -> Doc
$++$ forall {c :: * -> *} {a}. GInfo c a -> Doc
dConDoc   GInfo c a
x'
                  Doc -> Doc -> Doc
$++$ Doc
bindsDoc
                  Doc -> Doc -> Doc
$++$ forall {c :: * -> *} {a}. Fixpoint (c a) => GInfo c a -> Doc
csDoc    GInfo c a
x'
                  Doc -> Doc -> Doc
$++$ forall {a} {c :: * -> *}. Fixpoint a => GInfo c a -> Doc
wsDoc    GInfo c a
x'
                  Doc -> Doc -> Doc
$++$ GInfo c a -> Doc
binfoDoc GInfo c a
x'
                  Doc -> Doc -> Doc
$++$ [Char] -> Doc
text [Char]
"\n"
  where
    cfgDoc :: a -> Doc
cfgDoc a
cfg    = [Char] -> Doc
text ([Char]
"// " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
cfg)
    gConDoc :: GInfo c a -> Doc
gConDoc       = Doc -> SEnv Sort -> Doc
sEnvDoc Doc
"constant"             forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> SEnv Sort
gLits
    dConDoc :: GInfo c a -> Doc
dConDoc       = Doc -> SEnv Sort -> Doc
sEnvDoc Doc
"distinct"             forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> SEnv Sort
dLits
    csDoc :: GInfo c a -> Doc
csDoc         = [Doc] -> Doc
vcat     forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a. Fixpoint a => a -> Doc
toFix forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Ord a => HashMap a b -> [(a, b)]
hashMapToAscList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm
    wsDoc :: GInfo c a -> Doc
wsDoc         = [Doc] -> Doc
vcat     forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Fixpoint a => a -> Doc
toFix forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> [a] -> [a]
L.sortOn (forall a b c. (a, b, c) -> c
thd3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. WfC a -> (Symbol, Sort, KVar)
wrft) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. HashMap k v -> [v]
M.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws
    kutsDoc :: GInfo c a -> Doc
kutsDoc       = forall a. Fixpoint a => a -> Doc
toFix    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> Kuts
kuts
    -- packsDoc      = toFix    . packs
    declsDoc :: GInfo c a -> Doc
declsDoc      = [Doc] -> Doc
vcat     forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (([Char] -> Doc
text [Char]
"data" Doc -> Doc -> Doc
<+>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fixpoint a => a -> Doc
toFix) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
L.sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls
    (BindEnv a
ubs, EBindEnv a
ebs)    = forall a. BindEnv a -> [BindId] -> (BindEnv a, EBindEnv a)
splitByQuantifiers (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs GInfo c a
x') (forall (c :: * -> *) a. GInfo c a -> [BindId]
ebinds GInfo c a
x')
    bindsDoc :: Doc
bindsDoc      = forall a. Fixpoint a => a -> Doc
toFix    BindEnv a
ubs
               Doc -> Doc -> Doc
$++$ forall a. Fixpoint a => a -> Doc
toFix    EBindEnv a
ebs
    qualsDoc :: GInfo c a -> Doc
qualsDoc      = [Doc] -> Doc
vcat     forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Fixpoint a => a -> Doc
toFix forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
L.sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals
    aeDoc :: GInfo c a -> Doc
aeDoc         = forall a. Fixpoint a => a -> Doc
toFix    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae
    metaDoc :: (a, a) -> Doc
metaDoc (a
i,a
d) = Doc -> Doc -> Doc
toFixMeta ([Char] -> Doc
text [Char]
"bind" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix a
i) (forall a. Fixpoint a => a -> Doc
toFix a
d)
    mdata :: Bool
mdata         = Config -> Bool
metadata Config
cfg
    binfoDoc :: GInfo c a -> Doc
binfoDoc
      | Bool
mdata     = [Doc] -> Doc
vcat     forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a}. (Fixpoint a, Fixpoint a) => (a, a) -> Doc
metaDoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. HashMap k v -> [(k, v)]
M.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> HashMap BindId a
bindInfo
      | Bool
otherwise = \GInfo c a
_ -> [Char] -> Doc
text [Char]
"\n"

infixl 9 $++$
($++$) :: Doc -> Doc -> Doc
Doc
x $++$ :: Doc -> Doc -> Doc
$++$ Doc
y = Doc
x Doc -> Doc -> Doc
$+$ [Char] -> Doc
text [Char]
"\n" Doc -> Doc -> Doc
$+$ Doc
y

sEnvDoc :: Doc -> SEnv Sort -> Doc
sEnvDoc :: Doc -> SEnv Sort -> Doc
sEnvDoc Doc
d       = [Doc] -> Doc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Doc
kvD forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> [a] -> [a]
L.sortOn forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SEnv a -> [(Symbol, a)]
toListSEnv
  where
    kvD :: (Symbol, Sort) -> Doc
kvD (Symbol
c, Sort
so) = Doc
d Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Symbol
c Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (forall a. Fixpoint a => a -> Doc
toFix Sort
so)

writeFInfo :: (Fixpoint a, Fixpoint (c a)) => Config -> GInfo c a -> FilePath -> IO ()
writeFInfo :: forall a (c :: * -> *).
(Fixpoint a, Fixpoint (c a)) =>
Config -> GInfo c a -> [Char] -> IO ()
writeFInfo Config
cfg GInfo c a
fq [Char]
f = [Char] -> [Char] -> IO ()
writeFile [Char]
f (Doc -> [Char]
render forall a b. (a -> b) -> a -> b
$ forall a (c :: * -> *).
(Fixpoint a, Fixpoint (c a)) =>
Config -> GInfo c a -> Doc
toFixpoint Config
cfg GInfo c a
fq)

--------------------------------------------------------------------------------
-- | Query Conversions: FInfo to SInfo
--------------------------------------------------------------------------------
convertFormat :: (Fixpoint a) => FInfo a -> SInfo a
--------------------------------------------------------------------------------
convertFormat :: forall a. Fixpoint a => FInfo a -> SInfo a
convertFormat FInfo a
fi = FInfo a
fi' { cm :: HashMap SubcId (SimpC a)
cm = forall a. BindM -> SubC a -> SimpC a
subcToSimpc BindM
bindm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm FInfo a
fi' }
  where
    (BindM
bindm, FInfo a
fi') = forall a k v. (a -> k -> v -> a) -> a -> HashMap k v -> a
M.foldlWithKey' forall a. (BindM, FInfo a) -> SubcId -> SubC a -> (BindM, FInfo a)
outVV (forall k v. HashMap k v
M.empty, FInfo a
fi) forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm FInfo a
fi

subcToSimpc :: BindM -> SubC a -> SimpC a
subcToSimpc :: forall a. BindM -> SubC a -> SimpC a
subcToSimpc BindM
m SubC a
s = SimpC
  { _cenv :: IBindEnv
_cenv       = forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
s
  , _crhs :: Expr
_crhs       = Reft -> Expr
reftPred forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft forall a b. (a -> b) -> a -> b
$ forall a. SubC a -> SortedReft
srhs SubC a
s
  , _cid :: Maybe SubcId
_cid        = forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid SubC a
s
  , cbind :: BindId
cbind      = forall k v.
(?callStack::CallStack, Eq k, Hashable k) =>
[Char] -> k -> HashMap k v -> v
safeLookup [Char]
"subcToSimpc" (forall (c :: * -> *) a. TaggedC c a => c a -> SubcId
subcId SubC a
s) BindM
m
  , _ctag :: [BindId]
_ctag       = forall (c :: * -> *) a. TaggedC c a => c a -> [BindId]
stag SubC a
s
  , _cinfo :: a
_cinfo      = forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SubC a
s
  }

outVV :: (BindM, FInfo a) -> Integer -> SubC a -> (BindM, FInfo a)
outVV :: forall a. (BindM, FInfo a) -> SubcId -> SubC a -> (BindM, FInfo a)
outVV (BindM
m, FInfo a
fi) SubcId
i SubC a
c = (BindM
m', FInfo a
fi')
  where
    fi' :: FInfo a
fi'           = FInfo a
fi { bs :: BindEnv a
bs = BindEnv a
be', cm :: HashMap SubcId (SubC a)
cm = HashMap SubcId (SubC a)
cm' }
    m' :: BindM
m'            = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert SubcId
i BindId
bId BindM
m
    (BindId
bId, BindEnv a
be')    = forall a.
Symbol -> SortedReft -> a -> BindEnv a -> (BindId, BindEnv a)
insertBindEnv Symbol
x SortedReft
sr (forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SubC a
c) (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs FInfo a
fi)
    cm' :: HashMap SubcId (SubC a)
cm'           = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert SubcId
i SubC a
c' forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm FInfo a
fi
    c' :: SubC a
c'            = SubC a
c { _senv :: IBindEnv
_senv = [BindId] -> IBindEnv -> IBindEnv
insertsIBindEnv [BindId
bId] forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
c }
    sr :: SortedReft
sr            = forall a. SubC a -> SortedReft
slhs SubC a
c
    x :: Symbol
x             = Reft -> Symbol
reftBind forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft SortedReft
sr

type BindM = M.HashMap Integer BindId

sinfoToFInfo :: SInfo a -> FInfo a
sinfoToFInfo :: forall a. SInfo a -> FInfo a
sinfoToFInfo SInfo a
fi = SInfo a
fi
  { bs :: BindEnv a
bs = BindEnv a
envWithoutLhss
  , cm :: HashMap SubcId (SubC a)
cm = forall a. BindEnv a -> SimpC a -> SubC a
simpcToSubc (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
fi
  }
  where
    envWithoutLhss :: BindEnv a
envWithoutLhss =
      forall a v k. (a -> v -> a) -> a -> HashMap k v -> a
M.foldl' (\BindEnv a
m SimpC a
c -> forall a. BindId -> BindEnv a -> BindEnv a
deleteBindEnv (forall a. SimpC a -> BindId
cbind SimpC a
c) BindEnv a
m) (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi) (forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
fi)

-- Assumes the sort and the bind of the lhs is the same as the sort
-- and the bind of the rhs
simpcToSubc :: BindEnv a -> SimpC a -> SubC a
simpcToSubc :: forall a. BindEnv a -> SimpC a -> SubC a
simpcToSubc BindEnv a
env SimpC a
s = SubC
  { _senv :: IBindEnv
_senv  = BindId -> IBindEnv -> IBindEnv
deleteIBindEnv (forall a. SimpC a -> BindId
cbind SimpC a
s) (forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC a
s)
  , slhs :: SortedReft
slhs   = SortedReft
sr
  , srhs :: SortedReft
srhs   = Sort -> Reft -> SortedReft
RR (SortedReft -> Sort
sr_sort SortedReft
sr) ((Symbol, Expr) -> Reft
Reft (Symbol
b, forall a. SimpC a -> Expr
_crhs SimpC a
s))
  , _sid :: Maybe SubcId
_sid   = forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid SimpC a
s
  , _stag :: [BindId]
_stag  = forall (c :: * -> *) a. TaggedC c a => c a -> [BindId]
stag SimpC a
s
  , _sinfo :: a
_sinfo = forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SimpC a
s
  }
  where
    (Symbol
b, SortedReft
sr, a
_) = forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv (forall a. SimpC a -> BindId
cbind SimpC a
s) BindEnv a
env

---------------------------------------------------------------------------
-- | Top level Solvers ----------------------------------------------------
---------------------------------------------------------------------------
type Solver a = Config -> FInfo a -> IO (Result (Integer, a))

--------------------------------------------------------------------------------
saveQuery :: (Fixpoint a) => Config -> FInfo a -> IO ()
--------------------------------------------------------------------------------
saveQuery :: forall a. Fixpoint a => Config -> FInfo a -> IO ()
saveQuery Config
cfg FInfo a
fi = {- when (save cfg) $ -} do
  let fi' :: FInfo ()
fi'  = forall (f :: * -> *) a. Functor f => f a -> f ()
void FInfo a
fi
  Config -> FInfo () -> IO ()
saveBinaryQuery Config
cfg FInfo ()
fi'
  forall a. Fixpoint a => Config -> FInfo a -> IO ()
saveTextQuery Config
cfg   FInfo a
fi

saveBinaryQuery :: Config -> FInfo () -> IO ()
saveBinaryQuery :: Config -> FInfo () -> IO ()
saveBinaryQuery Config
cfg FInfo ()
fi = do
  let bfq :: [Char]
bfq  = Ext -> Config -> [Char]
queryFile Ext
Files.BinFq Config
cfg
  [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [Char]
"Saving Binary Query: " forall a. [a] -> [a] -> [a]
++ [Char]
bfq forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
  [Char] -> IO ()
ensurePath [Char]
bfq
  [Char] -> ByteString -> IO ()
B.writeFile [Char]
bfq (forall a. Store a => a -> ByteString
S.encode FInfo ()
fi)
  -- B.encodeFile bfq fi

saveTextQuery :: Fixpoint a => Config -> FInfo a -> IO ()
saveTextQuery :: forall a. Fixpoint a => Config -> FInfo a -> IO ()
saveTextQuery Config
cfg FInfo a
fi = do
  let fq :: [Char]
fq   = Ext -> Config -> [Char]
queryFile Ext
Files.Fq Config
cfg
  [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [Char]
"Saving Text Query: "   forall a. [a] -> [a] -> [a]
++ [Char]
fq forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
  [Char] -> IO ()
ensurePath [Char]
fq
  [Char] -> [Char] -> IO ()
writeFile [Char]
fq forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
render (forall a (c :: * -> *).
(Fixpoint a, Fixpoint (c a)) =>
Config -> GInfo c a -> Doc
toFixpoint Config
cfg FInfo a
fi)

---------------------------------------------------------------------------
-- | Axiom Instantiation Information --------------------------------------
---------------------------------------------------------------------------
data AxiomEnv = AEnv
  { AxiomEnv -> [Equation]
aenvEqs      :: ![Equation]
  , AxiomEnv -> [Rewrite]
aenvSimpl    :: ![Rewrite]
  , AxiomEnv -> HashMap SubcId Bool
aenvExpand   :: M.HashMap SubcId Bool
  , AxiomEnv -> HashMap SubcId [AutoRewrite]
aenvAutoRW   :: M.HashMap SubcId [AutoRewrite]
  } deriving (AxiomEnv -> AxiomEnv -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AxiomEnv -> AxiomEnv -> Bool
$c/= :: AxiomEnv -> AxiomEnv -> Bool
== :: AxiomEnv -> AxiomEnv -> Bool
$c== :: AxiomEnv -> AxiomEnv -> Bool
Eq, BindId -> AxiomEnv -> ShowS
[AxiomEnv] -> ShowS
AxiomEnv -> [Char]
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [AxiomEnv] -> ShowS
$cshowList :: [AxiomEnv] -> ShowS
show :: AxiomEnv -> [Char]
$cshow :: AxiomEnv -> [Char]
showsPrec :: BindId -> AxiomEnv -> ShowS
$cshowsPrec :: BindId -> AxiomEnv -> ShowS
Show, forall x. Rep AxiomEnv x -> AxiomEnv
forall x. AxiomEnv -> Rep AxiomEnv x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep AxiomEnv x -> AxiomEnv
$cfrom :: forall x. AxiomEnv -> Rep AxiomEnv x
Generic)

instance S.Store AutoRewrite
instance S.Store AxiomEnv
instance S.Store Rewrite
instance S.Store Equation
instance NFData AutoRewrite
instance NFData AxiomEnv
instance NFData Rewrite
instance NFData Equation

dedupAutoRewrites :: M.HashMap SubcId [AutoRewrite] -> [AutoRewrite]
dedupAutoRewrites :: HashMap SubcId [AutoRewrite] -> [AutoRewrite]
dedupAutoRewrites = forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. HashMap k v -> [v]
M.elems

instance Semigroup AxiomEnv where
  AxiomEnv
a1 <> :: AxiomEnv -> AxiomEnv -> AxiomEnv
<> AxiomEnv
a2        = [Equation]
-> [Rewrite]
-> HashMap SubcId Bool
-> HashMap SubcId [AutoRewrite]
-> AxiomEnv
AEnv [Equation]
aenvEqs' [Rewrite]
aenvSimpl' HashMap SubcId Bool
aenvExpand' HashMap SubcId [AutoRewrite]
aenvAutoRW'
    where
      aenvEqs' :: [Equation]
aenvEqs'    = AxiomEnv -> [Equation]
aenvEqs AxiomEnv
a1    forall a. Semigroup a => a -> a -> a
<> AxiomEnv -> [Equation]
aenvEqs AxiomEnv
a2
      aenvSimpl' :: [Rewrite]
aenvSimpl'  = AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
a1  forall a. Semigroup a => a -> a -> a
<> AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
a2
      aenvExpand' :: HashMap SubcId Bool
aenvExpand' = AxiomEnv -> HashMap SubcId Bool
aenvExpand AxiomEnv
a1 forall a. Semigroup a => a -> a -> a
<> AxiomEnv -> HashMap SubcId Bool
aenvExpand AxiomEnv
a2
      aenvAutoRW' :: HashMap SubcId [AutoRewrite]
aenvAutoRW' = AxiomEnv -> HashMap SubcId [AutoRewrite]
aenvAutoRW AxiomEnv
a1 forall a. Semigroup a => a -> a -> a
<> AxiomEnv -> HashMap SubcId [AutoRewrite]
aenvAutoRW AxiomEnv
a2

instance Monoid AxiomEnv where
  mempty :: AxiomEnv
mempty          = [Equation]
-> [Rewrite]
-> HashMap SubcId Bool
-> HashMap SubcId [AutoRewrite]
-> AxiomEnv
AEnv [] [] (forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList []) (forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [])
  mappend :: AxiomEnv -> AxiomEnv -> AxiomEnv
mappend         = forall a. Semigroup a => a -> a -> a
(<>)

instance PPrint AxiomEnv where
  pprintTidy :: Tidy -> AxiomEnv -> Doc
pprintTidy Tidy
_ = [Char] -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show

data Equation = Equ
  { Equation -> Symbol
eqName :: !Symbol           -- ^ name of reflected function
  , Equation -> [(Symbol, Sort)]
eqArgs :: [(Symbol, Sort)]  -- ^ names of parameters
  , Equation -> Expr
eqBody :: !Expr             -- ^ definition of body
  , Equation -> Sort
eqSort :: !Sort             -- ^ sort of body
  , Equation -> Bool
eqRec  :: !Bool             -- ^ is this a recursive definition
  }
  deriving (Typeable Equation
Equation -> DataType
Equation -> Constr
(forall b. Data b => b -> b) -> Equation -> Equation
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. BindId -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. BindId -> (forall d. Data d => d -> u) -> Equation -> u
forall u. (forall d. Data d => d -> u) -> Equation -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Equation -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Equation -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Equation
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Equation -> c Equation
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Equation)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Equation)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation
gmapQi :: forall u. BindId -> (forall d. Data d => d -> u) -> Equation -> u
$cgmapQi :: forall u. BindId -> (forall d. Data d => d -> u) -> Equation -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Equation -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Equation -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Equation -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Equation -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Equation -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Equation -> r
gmapT :: (forall b. Data b => b -> b) -> Equation -> Equation
$cgmapT :: (forall b. Data b => b -> b) -> Equation -> Equation
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Equation)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Equation)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Equation)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Equation)
dataTypeOf :: Equation -> DataType
$cdataTypeOf :: Equation -> DataType
toConstr :: Equation -> Constr
$ctoConstr :: Equation -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Equation
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Equation
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Equation -> c Equation
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Equation -> c Equation
Data, Equation -> Equation -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Equation -> Equation -> Bool
$c/= :: Equation -> Equation -> Bool
== :: Equation -> Equation -> Bool
$c== :: Equation -> Equation -> Bool
Eq, Eq Equation
Equation -> Equation -> Bool
Equation -> Equation -> Ordering
Equation -> Equation -> Equation
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Equation -> Equation -> Equation
$cmin :: Equation -> Equation -> Equation
max :: Equation -> Equation -> Equation
$cmax :: Equation -> Equation -> Equation
>= :: Equation -> Equation -> Bool
$c>= :: Equation -> Equation -> Bool
> :: Equation -> Equation -> Bool
$c> :: Equation -> Equation -> Bool
<= :: Equation -> Equation -> Bool
$c<= :: Equation -> Equation -> Bool
< :: Equation -> Equation -> Bool
$c< :: Equation -> Equation -> Bool
compare :: Equation -> Equation -> Ordering
$ccompare :: Equation -> Equation -> Ordering
Ord, BindId -> Equation -> ShowS
[Equation] -> ShowS
Equation -> [Char]
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Equation] -> ShowS
$cshowList :: [Equation] -> ShowS
show :: Equation -> [Char]
$cshow :: Equation -> [Char]
showsPrec :: BindId -> Equation -> ShowS
$cshowsPrec :: BindId -> Equation -> ShowS
Show, forall x. Rep Equation x -> Equation
forall x. Equation -> Rep Equation x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Equation x -> Equation
$cfrom :: forall x. Equation -> Rep Equation x
Generic)

mkEquation :: Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
mkEquation :: Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
mkEquation Symbol
f [(Symbol, Sort)]
xts Expr
e Sort
out = Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Bool -> Equation
Equ Symbol
f [(Symbol, Sort)]
xts Expr
e Sort
out (Symbol
f forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a. Subable a => a -> [Symbol]
syms Expr
e)

instance Subable Equation where
  syms :: Equation -> [Symbol]
syms   Equation
a = forall a. Subable a => a -> [Symbol]
syms (Equation -> Expr
eqBody Equation
a) -- ++ F.syms (axiomEq a)
  subst :: Subst -> Equation -> Equation
subst Subst
su = (Expr -> Expr) -> Equation -> Equation
mapEqBody (forall a. Subable a => Subst -> a -> a
subst Subst
su)
  substf :: (Symbol -> Expr) -> Equation -> Equation
substf Symbol -> Expr
f = (Expr -> Expr) -> Equation -> Equation
mapEqBody (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f)
  substa :: (Symbol -> Symbol) -> Equation -> Equation
substa Symbol -> Symbol
f = (Expr -> Expr) -> Equation -> Equation
mapEqBody (forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
f)

mapEqBody :: (Expr -> Expr) -> Equation -> Equation
mapEqBody :: (Expr -> Expr) -> Equation -> Equation
mapEqBody Expr -> Expr
f Equation
a = Equation
a { eqBody :: Expr
eqBody = Expr -> Expr
f (Equation -> Expr
eqBody Equation
a) }

instance PPrint Equation where
  pprintTidy :: Tidy -> Equation -> Doc
pprintTidy Tidy
_ = forall a. Fixpoint a => a -> Doc
toFix

ppArgs :: (PPrint a) => [a] -> Doc
ppArgs :: forall a. PPrint a => [a] -> Doc
ppArgs = Doc -> Doc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> Doc
intersperse Doc
", " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. PPrint a => a -> Doc
pprint


data AutoRewrite = AutoRewrite
  { AutoRewrite -> [SortedReft]
arArgs :: [SortedReft]
  , AutoRewrite -> Expr
arLHS  :: Expr
  , AutoRewrite -> Expr
arRHS  :: Expr
} deriving (AutoRewrite -> AutoRewrite -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AutoRewrite -> AutoRewrite -> Bool
$c/= :: AutoRewrite -> AutoRewrite -> Bool
== :: AutoRewrite -> AutoRewrite -> Bool
$c== :: AutoRewrite -> AutoRewrite -> Bool
Eq, Eq AutoRewrite
AutoRewrite -> AutoRewrite -> Bool
AutoRewrite -> AutoRewrite -> Ordering
AutoRewrite -> AutoRewrite -> AutoRewrite
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: AutoRewrite -> AutoRewrite -> AutoRewrite
$cmin :: AutoRewrite -> AutoRewrite -> AutoRewrite
max :: AutoRewrite -> AutoRewrite -> AutoRewrite
$cmax :: AutoRewrite -> AutoRewrite -> AutoRewrite
>= :: AutoRewrite -> AutoRewrite -> Bool
$c>= :: AutoRewrite -> AutoRewrite -> Bool
> :: AutoRewrite -> AutoRewrite -> Bool
$c> :: AutoRewrite -> AutoRewrite -> Bool
<= :: AutoRewrite -> AutoRewrite -> Bool
$c<= :: AutoRewrite -> AutoRewrite -> Bool
< :: AutoRewrite -> AutoRewrite -> Bool
$c< :: AutoRewrite -> AutoRewrite -> Bool
compare :: AutoRewrite -> AutoRewrite -> Ordering
$ccompare :: AutoRewrite -> AutoRewrite -> Ordering
Ord, BindId -> AutoRewrite -> ShowS
[AutoRewrite] -> ShowS
AutoRewrite -> [Char]
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [AutoRewrite] -> ShowS
$cshowList :: [AutoRewrite] -> ShowS
show :: AutoRewrite -> [Char]
$cshow :: AutoRewrite -> [Char]
showsPrec :: BindId -> AutoRewrite -> ShowS
$cshowsPrec :: BindId -> AutoRewrite -> ShowS
Show, forall x. Rep AutoRewrite x -> AutoRewrite
forall x. AutoRewrite -> Rep AutoRewrite x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep AutoRewrite x -> AutoRewrite
$cfrom :: forall x. AutoRewrite -> Rep AutoRewrite x
Generic)

instance Hashable AutoRewrite


instance Fixpoint (M.HashMap SubcId [AutoRewrite]) where
  toFix :: HashMap SubcId [AutoRewrite] -> Doc
toFix HashMap SubcId [AutoRewrite]
autoRW =
    [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$
    forall a b. (a -> b) -> [a] -> [b]
map AutoRewrite -> Doc
fixRW [AutoRewrite]
rewrites forall a. [a] -> [a] -> [a]
++
    [Doc]
rwsMapping
    where
      rewrites :: [AutoRewrite]
rewrites = HashMap SubcId [AutoRewrite] -> [AutoRewrite]
dedupAutoRewrites HashMap SubcId [AutoRewrite]
autoRW

      fixRW :: AutoRewrite -> Doc
fixRW rw :: AutoRewrite
rw@(AutoRewrite [SortedReft]
args Expr
lhs Expr
rhs) =
          [Char] -> Doc
text ([Char]
"autorewrite " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. Hashable a => a -> BindId
hash AutoRewrite
rw))
          Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Fixpoint a => a -> Doc
toFix [SortedReft]
args)
          Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"="
          Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"{"
          Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Expr
lhs
          Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"="
          Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Expr
rhs
          Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"}"

      rwsMapping :: [Doc]
rwsMapping = do
        (SubcId
cid, [AutoRewrite]
rws) <- forall k v. HashMap k v -> [(k, v)]
M.toList HashMap SubcId [AutoRewrite]
autoRW
        AutoRewrite
rw         <-  [AutoRewrite]
rws
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Doc
"rewrite" Doc -> Doc -> Doc
<+> Doc -> Doc
brackets ([Char] -> Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show SubcId
cid forall a. [a] -> [a] -> [a]
++ [Char]
" : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. Hashable a => a -> BindId
hash AutoRewrite
rw))



-- eg  SMeasure (f D [x1..xn] e)
-- for f (D x1 .. xn) = e
data Rewrite  = SMeasure
  { Rewrite -> Symbol
smName  :: Symbol         -- eg. f
  , Rewrite -> Symbol
smDC    :: Symbol         -- eg. D
  , Rewrite -> [Symbol]
smArgs  :: [Symbol]       -- eg. xs
  , Rewrite -> Expr
smBody  :: Expr           -- eg. e[xs]
  }
  deriving (Typeable Rewrite
Rewrite -> DataType
Rewrite -> Constr
(forall b. Data b => b -> b) -> Rewrite -> Rewrite
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. BindId -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. BindId -> (forall d. Data d => d -> u) -> Rewrite -> u
forall u. (forall d. Data d => d -> u) -> Rewrite -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Rewrite -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Rewrite -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Rewrite
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rewrite -> c Rewrite
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Rewrite)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Rewrite)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
gmapQi :: forall u. BindId -> (forall d. Data d => d -> u) -> Rewrite -> u
$cgmapQi :: forall u. BindId -> (forall d. Data d => d -> u) -> Rewrite -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Rewrite -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Rewrite -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Rewrite -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Rewrite -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Rewrite -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Rewrite -> r
gmapT :: (forall b. Data b => b -> b) -> Rewrite -> Rewrite
$cgmapT :: (forall b. Data b => b -> b) -> Rewrite -> Rewrite
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Rewrite)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Rewrite)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Rewrite)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Rewrite)
dataTypeOf :: Rewrite -> DataType
$cdataTypeOf :: Rewrite -> DataType
toConstr :: Rewrite -> Constr
$ctoConstr :: Rewrite -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Rewrite
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Rewrite
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rewrite -> c Rewrite
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rewrite -> c Rewrite
Data, Rewrite -> Rewrite -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rewrite -> Rewrite -> Bool
$c/= :: Rewrite -> Rewrite -> Bool
== :: Rewrite -> Rewrite -> Bool
$c== :: Rewrite -> Rewrite -> Bool
Eq, Eq Rewrite
Rewrite -> Rewrite -> Bool
Rewrite -> Rewrite -> Ordering
Rewrite -> Rewrite -> Rewrite
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Rewrite -> Rewrite -> Rewrite
$cmin :: Rewrite -> Rewrite -> Rewrite
max :: Rewrite -> Rewrite -> Rewrite
$cmax :: Rewrite -> Rewrite -> Rewrite
>= :: Rewrite -> Rewrite -> Bool
$c>= :: Rewrite -> Rewrite -> Bool
> :: Rewrite -> Rewrite -> Bool
$c> :: Rewrite -> Rewrite -> Bool
<= :: Rewrite -> Rewrite -> Bool
$c<= :: Rewrite -> Rewrite -> Bool
< :: Rewrite -> Rewrite -> Bool
$c< :: Rewrite -> Rewrite -> Bool
compare :: Rewrite -> Rewrite -> Ordering
$ccompare :: Rewrite -> Rewrite -> Ordering
Ord, BindId -> Rewrite -> ShowS
[Rewrite] -> ShowS
Rewrite -> [Char]
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Rewrite] -> ShowS
$cshowList :: [Rewrite] -> ShowS
show :: Rewrite -> [Char]
$cshow :: Rewrite -> [Char]
showsPrec :: BindId -> Rewrite -> ShowS
$cshowsPrec :: BindId -> Rewrite -> ShowS
Show, forall x. Rep Rewrite x -> Rewrite
forall x. Rewrite -> Rep Rewrite x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Rewrite x -> Rewrite
$cfrom :: forall x. Rewrite -> Rep Rewrite x
Generic)

instance Fixpoint AxiomEnv where
  toFix :: AxiomEnv -> Doc
toFix AxiomEnv
axe = [Doc] -> Doc
vcat ((forall a. Fixpoint a => a -> Doc
toFix forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Ord a => [a] -> [a]
L.sort (AxiomEnv -> [Equation]
aenvEqs AxiomEnv
axe)) forall a. [a] -> [a] -> [a]
++ (forall a. Fixpoint a => a -> Doc
toFix forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Ord a => [a] -> [a]
L.sort (AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
axe)))
              Doc -> Doc -> Doc
$+$ forall {a}. Fixpoint a => [a] -> Doc
renderExpand (forall {a} {a}. (Show a, Show a) => (a, a) -> Doc
pairdoc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Ord a => [a] -> [a]
L.sort (forall k v. HashMap k v -> [(k, v)]
M.toList forall a b. (a -> b) -> a -> b
$ AxiomEnv -> HashMap SubcId Bool
aenvExpand AxiomEnv
axe))
              Doc -> Doc -> Doc
$+$ forall a. Fixpoint a => a -> Doc
toFix (AxiomEnv -> HashMap SubcId [AutoRewrite]
aenvAutoRW AxiomEnv
axe)
    where
      pairdoc :: (a, a) -> Doc
pairdoc (a
x,a
y) = [Char] -> Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show a
x forall a. [a] -> [a] -> [a]
++ [Char]
" : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
y
      renderExpand :: [a] -> Doc
renderExpand [] = Doc
empty
      renderExpand [a]
xs = [Char] -> Doc
text [Char]
"expand" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix [a]
xs

instance Fixpoint Equation where
  toFix :: Equation -> Doc
toFix (Equ Symbol
f [(Symbol, Sort)]
xs Expr
e Sort
s Bool
_) = Doc
"define" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Symbol
f Doc -> Doc -> Doc
<+> forall a. PPrint a => [a] -> Doc
ppArgs [(Symbol, Sort)]
xs Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Sort
s Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"=" Doc -> Doc -> Doc
<+> Doc -> Doc
braces (Doc -> Doc
parens (forall a. Fixpoint a => a -> Doc
toFix Expr
e))

instance Fixpoint Rewrite where
  toFix :: Rewrite -> Doc
toFix (SMeasure Symbol
f Symbol
d [Symbol]
xs Expr
e)
    = [Char] -> Doc
text [Char]
"match"
   Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Symbol
f
   Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Symbol
d Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep (forall a. Fixpoint a => a -> Doc
toFix forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs)
   Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
" = "
   Doc -> Doc -> Doc
<+> Doc -> Doc
parens (forall a. Fixpoint a => a -> Doc
toFix Expr
e)

instance PPrint Rewrite where
  pprintTidy :: Tidy -> Rewrite -> Doc
pprintTidy Tidy
_ = forall a. Fixpoint a => a -> Doc
toFix