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

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

-- | 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

   -- * Serializing
  , toFixpoint
  , writeFInfo
  , saveQuery
  , saveSInfo

   -- * Constructing Queries
  , fi

  -- * Constraints
  , WfC (..)
  , 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

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

  -- * Results
  , FixSolution
  , FixDelayedSolution
  , Delayed (..)
  , Result (..), ResultSorts
  , unsafe, isUnsafe, isSafe ,safe

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

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

  -- * Axioms
  , AxiomEnv (..)
  , Equation
  , DefinedFuns (..)
  , EquationV (..)
  , mkEquation
  , Rewrite  (..)
  , AutoRewrite (..)
  , dedupAutoRewrites
  , LocalRewritesEnv (..)
  , LocalRewrites (..)
  , lookupRewrite
  , lookupLocalRewrites
  , insertRewrites
  , eqnToHornSMT

  -- * 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             (when, void)
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.SMTPrint
import qualified Language.Fixpoint.Types.Config as C
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.Text as T
import qualified Data.Text.IO as T
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
                    }
              deriving (WfC a -> WfC a -> Bool
(WfC a -> WfC a -> Bool) -> (WfC a -> WfC a -> Bool) -> Eq (WfC a)
forall a. Eq a => WfC a -> WfC a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: WfC a -> WfC a -> Bool
Eq, (forall x. WfC a -> Rep (WfC a) x)
-> (forall x. Rep (WfC a) x -> WfC a) -> Generic (WfC a)
forall x. Rep (WfC a) x -> WfC a
forall x. WfC a -> Rep (WfC a) x
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
$cfrom :: forall a x. WfC a -> Rep (WfC a) x
from :: forall x. WfC a -> Rep (WfC a) x
$cto :: forall a x. Rep (WfC a) x -> WfC a
to :: forall x. Rep (WfC a) x -> WfC a
Generic, (forall a b. (a -> b) -> WfC a -> WfC b)
-> (forall a b. a -> WfC b -> WfC a) -> Functor WfC
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
$cfmap :: forall a b. (a -> b) -> WfC a -> WfC b
fmap :: forall a b. (a -> b) -> WfC a -> WfC b
$c<$ :: forall a b. a -> WfC b -> WfC a
<$ :: forall a b. a -> WfC b -> WfC a
Functor)

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 Integer
_sid   :: !(Maybe SubcId)
  , forall a. SubC a -> Tag
_stag  :: !Tag
  , forall a. SubC a -> a
_sinfo :: !a
  }
  deriving (SubC a -> SubC a -> Bool
(SubC a -> SubC a -> Bool)
-> (SubC a -> SubC a -> Bool) -> Eq (SubC a)
forall a. Eq a => SubC a -> SubC a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: SubC a -> SubC a -> Bool
Eq, (forall x. SubC a -> Rep (SubC a) x)
-> (forall x. Rep (SubC a) x -> SubC a) -> Generic (SubC a)
forall x. Rep (SubC a) x -> SubC a
forall x. SubC a -> Rep (SubC a) x
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
$cfrom :: forall a x. SubC a -> Rep (SubC a) x
from :: forall x. SubC a -> Rep (SubC a) x
$cto :: forall a x. Rep (SubC a) x -> SubC a
to :: forall x. Rep (SubC a) x -> SubC a
Generic, (forall a b. (a -> b) -> SubC a -> SubC b)
-> (forall a b. a -> SubC b -> SubC a) -> Functor SubC
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
$cfmap :: forall a b. (a -> b) -> SubC a -> SubC b
fmap :: forall a b. (a -> b) -> SubC a -> SubC b
$c<$ :: forall a b. a -> SubC b -> SubC a
<$ :: forall a b. a -> SubC b -> SubC a
Functor)

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

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

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

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


strengthenBinds :: SInfo a -> M.HashMap BindId Expr -> BindEnv a
strengthenBinds :: forall a. SInfo a -> HashMap BindId Expr -> BindEnv a
strengthenBinds SInfo a
si HashMap BindId Expr
m = (BindId -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a))
-> BindEnv a -> BindEnv a
forall a.
(BindId -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a))
-> BindEnv a -> BindEnv a
mapBindEnv BindId -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a)
f (SInfo a -> BindEnv a
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 BindId -> HashMap BindId Expr -> Maybe Expr
forall k v. 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 -> ReftV Symbol -> SortedReft
RR Sort
s ((Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
v, ListNE Expr -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
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      = SimpC a -> IBindEnv
forall a. SimpC a -> IBindEnv
_cenv
  updateSEnv :: SimpC a -> (IBindEnv -> IBindEnv) -> SimpC a
updateSEnv SimpC a
c IBindEnv -> IBindEnv
f = SimpC a
c { _cenv = f (_cenv c) }
  sid :: SimpC a -> Maybe Integer
sid       = SimpC a -> Maybe Integer
forall a. SimpC a -> Maybe Integer
_cid
  stag :: SimpC a -> Tag
stag      = SimpC a -> Tag
forall a. SimpC a -> Tag
_ctag
  sinfo :: SimpC a -> a
sinfo     = SimpC a -> a
forall a. SimpC a -> a
_cinfo
  crhs :: SimpC a -> Expr
crhs      = SimpC a -> Expr
forall a. SimpC a -> Expr
_crhs
  clhs :: BindEnv a -> SimpC a -> [(Symbol, SortedReft)]
clhs BindEnv a
be SimpC a
c = BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
envCs BindEnv a
be (SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC a
c)

instance TaggedC SubC a where
  senv :: SubC a -> IBindEnv
senv      = SubC a -> IBindEnv
forall a. SubC a -> IBindEnv
_senv
  updateSEnv :: SubC a -> (IBindEnv -> IBindEnv) -> SubC a
updateSEnv SubC a
c IBindEnv -> IBindEnv
f = SubC a
c { _senv = f (_senv c) }
  sid :: SubC a -> Maybe Integer
sid       = SubC a -> Maybe Integer
forall a. SubC a -> Maybe Integer
_sid
  stag :: SubC a -> Tag
stag      = SubC a -> Tag
forall a. SubC a -> Tag
_stag
  sinfo :: SubC a -> a
sinfo     = SubC a -> a
forall a. SubC a -> a
_sinfo
  crhs :: SubC a -> Expr
crhs      = ReftV Symbol -> Expr
forall v. ReftV v -> ExprV v
reftPred (ReftV Symbol -> Expr)
-> (SubC a -> ReftV Symbol) -> SubC a -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> ReftV Symbol
sr_reft (SortedReft -> ReftV Symbol)
-> (SubC a -> SortedReft) -> SubC a -> ReftV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs
  clhs :: BindEnv a -> SubC a -> [(Symbol, SortedReft)]
clhs BindEnv a
be SubC a
c = SortedReft -> (Symbol, SortedReft)
sortedReftBind (SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
c) (Symbol, SortedReft)
-> [(Symbol, SortedReft)] -> [(Symbol, SortedReft)]
forall a. a -> [a] -> [a]
: BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
envCs BindEnv a
be (SubC a -> IBindEnv
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 -> ReftV Symbol
sr_reft SortedReft
sr

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

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

-- | Since some solutions are expensive to compute, we wrap them in a
-- "Delayed" type to compute them only if needed.
{- HLINT ignore Delayed "Use newtype instead of data" -}
data Delayed a = Delayed
  { forall a. Delayed a -> a
forceDelayed  :: a
  }
  deriving ((forall x. Delayed a -> Rep (Delayed a) x)
-> (forall x. Rep (Delayed a) x -> Delayed a)
-> Generic (Delayed a)
forall x. Rep (Delayed a) x -> Delayed a
forall x. Delayed a -> Rep (Delayed a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Delayed a) x -> Delayed a
forall a x. Delayed a -> Rep (Delayed a) x
$cfrom :: forall a x. Delayed a -> Rep (Delayed a) x
from :: forall x. Delayed a -> Rep (Delayed a) x
$cto :: forall a x. Rep (Delayed a) x -> Delayed a
to :: forall x. Rep (Delayed a) x -> Delayed a
Generic, BindId -> Delayed a -> [Char] -> [Char]
[Delayed a] -> [Char] -> [Char]
Delayed a -> [Char]
(BindId -> Delayed a -> [Char] -> [Char])
-> (Delayed a -> [Char])
-> ([Delayed a] -> [Char] -> [Char])
-> Show (Delayed a)
forall a. Show a => BindId -> Delayed a -> [Char] -> [Char]
forall a. Show a => [Delayed a] -> [Char] -> [Char]
forall a. Show a => Delayed a -> [Char]
forall a.
(BindId -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: forall a. Show a => BindId -> Delayed a -> [Char] -> [Char]
showsPrec :: BindId -> Delayed a -> [Char] -> [Char]
$cshow :: forall a. Show a => Delayed a -> [Char]
show :: Delayed a -> [Char]
$cshowList :: forall a. Show a => [Delayed a] -> [Char] -> [Char]
showList :: [Delayed a] -> [Char] -> [Char]
Show, (forall a b. (a -> b) -> Delayed a -> Delayed b)
-> (forall a b. a -> Delayed b -> Delayed a) -> Functor Delayed
forall a b. a -> Delayed b -> Delayed a
forall a b. (a -> b) -> Delayed a -> Delayed b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Delayed a -> Delayed b
fmap :: forall a b. (a -> b) -> Delayed a -> Delayed b
$c<$ :: forall a b. a -> Delayed b -> Delayed a
<$ :: forall a b. a -> Delayed b -> Delayed a
Functor)

instance (NFData a) => NFData (Delayed a)


type FixSolution  = M.HashMap KVar Expr
type FixDelayedSolution  = M.HashMap KVar (Delayed Expr)

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

type ResultSorts = M.HashMap KVar [(Symbol, Sort)]

data ScopedResult = MkScopedResult
  { ScopedResult -> KVarMap ScopedExpr
scCuts    :: KVarMap ScopedExpr
  , ScopedResult -> KVarMap ScopedExpr
scNonCuts :: KVarMap ScopedExpr
  }
  deriving ((forall x. ScopedResult -> Rep ScopedResult x)
-> (forall x. Rep ScopedResult x -> ScopedResult)
-> Generic ScopedResult
forall x. Rep ScopedResult x -> ScopedResult
forall x. ScopedResult -> Rep ScopedResult x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ScopedResult -> Rep ScopedResult x
from :: forall x. ScopedResult -> Rep ScopedResult x
$cto :: forall x. Rep ScopedResult x -> ScopedResult
to :: forall x. Rep ScopedResult x -> ScopedResult
Generic, BindId -> ScopedResult -> [Char] -> [Char]
[ScopedResult] -> [Char] -> [Char]
ScopedResult -> [Char]
(BindId -> ScopedResult -> [Char] -> [Char])
-> (ScopedResult -> [Char])
-> ([ScopedResult] -> [Char] -> [Char])
-> Show ScopedResult
forall a.
(BindId -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: BindId -> ScopedResult -> [Char] -> [Char]
showsPrec :: BindId -> ScopedResult -> [Char] -> [Char]
$cshow :: ScopedResult -> [Char]
show :: ScopedResult -> [Char]
$cshowList :: [ScopedResult] -> [Char] -> [Char]
showList :: [ScopedResult] -> [Char] -> [Char]
Show)

newtype KVarMap a = MkKVarMap { forall a. KVarMap a -> HashMap KVar a
unKVarMap :: M.HashMap KVar a }
  deriving ((forall x. KVarMap a -> Rep (KVarMap a) x)
-> (forall x. Rep (KVarMap a) x -> KVarMap a)
-> Generic (KVarMap a)
forall x. Rep (KVarMap a) x -> KVarMap a
forall x. KVarMap a -> Rep (KVarMap a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (KVarMap a) x -> KVarMap a
forall a x. KVarMap a -> Rep (KVarMap a) x
$cfrom :: forall a x. KVarMap a -> Rep (KVarMap a) x
from :: forall x. KVarMap a -> Rep (KVarMap a) x
$cto :: forall a x. Rep (KVarMap a) x -> KVarMap a
to :: forall x. Rep (KVarMap a) x -> KVarMap a
Generic, BindId -> KVarMap a -> [Char] -> [Char]
[KVarMap a] -> [Char] -> [Char]
KVarMap a -> [Char]
(BindId -> KVarMap a -> [Char] -> [Char])
-> (KVarMap a -> [Char])
-> ([KVarMap a] -> [Char] -> [Char])
-> Show (KVarMap a)
forall a. Show a => BindId -> KVarMap a -> [Char] -> [Char]
forall a. Show a => [KVarMap a] -> [Char] -> [Char]
forall a. Show a => KVarMap a -> [Char]
forall a.
(BindId -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: forall a. Show a => BindId -> KVarMap a -> [Char] -> [Char]
showsPrec :: BindId -> KVarMap a -> [Char] -> [Char]
$cshow :: forall a. Show a => KVarMap a -> [Char]
show :: KVarMap a -> [Char]
$cshowList :: forall a. Show a => [KVarMap a] -> [Char] -> [Char]
showList :: [KVarMap a] -> [Char] -> [Char]
Show)

newtype KVarBind a = MkKVarBind { forall a. KVarBind a -> (KVar, a)
unKVarBind :: (KVar, a) }
  deriving ((forall x. KVarBind a -> Rep (KVarBind a) x)
-> (forall x. Rep (KVarBind a) x -> KVarBind a)
-> Generic (KVarBind a)
forall x. Rep (KVarBind a) x -> KVarBind a
forall x. KVarBind a -> Rep (KVarBind a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (KVarBind a) x -> KVarBind a
forall a x. KVarBind a -> Rep (KVarBind a) x
$cfrom :: forall a x. KVarBind a -> Rep (KVarBind a) x
from :: forall x. KVarBind a -> Rep (KVarBind a) x
$cto :: forall a x. Rep (KVarBind a) x -> KVarBind a
to :: forall x. Rep (KVarBind a) x -> KVarBind a
Generic, BindId -> KVarBind a -> [Char] -> [Char]
[KVarBind a] -> [Char] -> [Char]
KVarBind a -> [Char]
(BindId -> KVarBind a -> [Char] -> [Char])
-> (KVarBind a -> [Char])
-> ([KVarBind a] -> [Char] -> [Char])
-> Show (KVarBind a)
forall a. Show a => BindId -> KVarBind a -> [Char] -> [Char]
forall a. Show a => [KVarBind a] -> [Char] -> [Char]
forall a. Show a => KVarBind a -> [Char]
forall a.
(BindId -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: forall a. Show a => BindId -> KVarBind a -> [Char] -> [Char]
showsPrec :: BindId -> KVarBind a -> [Char] -> [Char]
$cshow :: forall a. Show a => KVarBind a -> [Char]
show :: KVarBind a -> [Char]
$cshowList :: forall a. Show a => [KVarBind a] -> [Char] -> [Char]
showList :: [KVarBind a] -> [Char] -> [Char]
Show)
data ScopedExpr = MkScopedExpr
  { ScopedExpr -> [(Symbol, Sort)]
seParams :: [(Symbol, Sort)]
  , ScopedExpr -> Expr
seBody :: !Expr
  }
  deriving ((forall x. ScopedExpr -> Rep ScopedExpr x)
-> (forall x. Rep ScopedExpr x -> ScopedExpr) -> Generic ScopedExpr
forall x. Rep ScopedExpr x -> ScopedExpr
forall x. ScopedExpr -> Rep ScopedExpr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ScopedExpr -> Rep ScopedExpr x
from :: forall x. ScopedExpr -> Rep ScopedExpr x
$cto :: forall x. Rep ScopedExpr x -> ScopedExpr
to :: forall x. Rep ScopedExpr x -> ScopedExpr
Generic, BindId -> ScopedExpr -> [Char] -> [Char]
[ScopedExpr] -> [Char] -> [Char]
ScopedExpr -> [Char]
(BindId -> ScopedExpr -> [Char] -> [Char])
-> (ScopedExpr -> [Char])
-> ([ScopedExpr] -> [Char] -> [Char])
-> Show ScopedExpr
forall a.
(BindId -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: BindId -> ScopedExpr -> [Char] -> [Char]
showsPrec :: BindId -> ScopedExpr -> [Char] -> [Char]
$cshow :: ScopedExpr -> [Char]
show :: ScopedExpr -> [Char]
$cshowList :: [ScopedExpr] -> [Char] -> [Char]
showList :: [ScopedExpr] -> [Char] -> [Char]
Show)

instance ToHornSMT ScopedExpr where
  toHornSMT :: ScopedExpr -> Doc
toHornSMT (MkScopedExpr [(Symbol, Sort)]
xts Expr
p) = Doc -> [(Symbol, Sort)] -> Expr -> Doc
forall a t.
(ToHornSMT a, ToHornSMT t) =>
Doc -> [(Symbol, t)] -> a -> Doc
toHornWithBinders Doc
"lambda" [(Symbol, Sort)]
xts Expr
p


scopedResult :: Result a -> ScopedResult
scopedResult :: forall a. Result a -> ScopedResult
scopedResult Result a
res = KVarMap ScopedExpr -> KVarMap ScopedExpr -> ScopedResult
MkScopedResult KVarMap ScopedExpr
cuts  KVarMap ScopedExpr
nonCuts
  where
    cuts :: KVarMap ScopedExpr
cuts = FixSolution -> KVarMap ScopedExpr
scoped (FixSolution -> KVarMap ScopedExpr)
-> FixSolution -> KVarMap ScopedExpr
forall a b. (a -> b) -> a -> b
$ Result a -> FixSolution
forall a. Result a -> FixSolution
resSolution Result a
res
    nonCuts :: KVarMap ScopedExpr
nonCuts = FixSolution -> KVarMap ScopedExpr
scoped (FixSolution -> KVarMap ScopedExpr)
-> FixSolution -> KVarMap ScopedExpr
forall a b. (a -> b) -> a -> b
$ (Delayed Expr -> Expr) -> FixDelayedSolution -> FixSolution
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map Delayed Expr -> Expr
forall a. Delayed a -> a
forceDelayed (FixDelayedSolution -> FixSolution)
-> FixDelayedSolution -> FixSolution
forall a b. (a -> b) -> a -> b
$ Result a -> FixDelayedSolution
forall a. Result a -> FixDelayedSolution
resNonCutsSolution Result a
res
    scoped :: FixSolution -> KVarMap ScopedExpr
scoped FixSolution
sol = HashMap KVar ScopedExpr -> KVarMap ScopedExpr
forall a. HashMap KVar a -> KVarMap a
MkKVarMap (HashMap KVar ScopedExpr -> KVarMap ScopedExpr)
-> HashMap KVar ScopedExpr -> KVarMap ScopedExpr
forall a b. (a -> b) -> a -> b
$ [(KVar, ScopedExpr)] -> HashMap KVar ScopedExpr
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [ (KVar
k, [(Symbol, Sort)] -> Expr -> ScopedExpr
MkScopedExpr (KVar -> [(Symbol, Sort)]
scope KVar
k) Expr
e) | (KVar
k, Expr
e) <- FixSolution -> [(KVar, Expr)]
forall k v. HashMap k v -> [(k, v)]
M.toList FixSolution
sol]
    scope :: KVar -> [(Symbol, Sort)]
scope KVar
k = [(Symbol, Sort)] -> KVar -> ResultSorts -> [(Symbol, Sort)]
forall k v. Hashable k => v -> k -> HashMap k v -> v
M.lookupDefault [] KVar
k (ResultSorts -> [(Symbol, Sort)])
-> ResultSorts -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ Result a -> ResultSorts
forall a. Result a -> ResultSorts
resSorts Result a
res

instance ToJSON a => ToJSON (Result a) where
  toJSON :: Result a -> Value
toJSON r :: Result a
r@(Result {ResultSorts
FixSolution
FixDelayedSolution
FixResult a
resStatus :: forall a. Result a -> FixResult a
resSolution :: forall a. Result a -> FixSolution
resNonCutsSolution :: forall a. Result a -> FixDelayedSolution
resSorts :: forall a. Result a -> ResultSorts
resStatus :: FixResult a
resSolution :: FixSolution
resNonCutsSolution :: FixDelayedSolution
resSorts :: ResultSorts
..}) = [Pair] -> Value
object
    [ Key
"status"            Key -> FixResult a -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= FixResult a
resStatus
    , Key
"solution"          Key -> KVarMap ScopedExpr -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= ScopedResult -> KVarMap ScopedExpr
scCuts ScopedResult
scopedSolution
    , Key
"nonCutsSolution"   Key -> KVarMap ScopedExpr -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= ScopedResult -> KVarMap ScopedExpr
scNonCuts ScopedResult
scopedSolution
    ]
    where
      scopedSolution :: ScopedResult
scopedSolution = Result a -> ScopedResult
forall a. Result a -> ScopedResult
scopedResult Result a
r

instance ToJSON a => ToJSON (KVarBind a) where
  toJSON :: KVarBind a -> Value
toJSON (MkKVarBind (KVar
k, a
v)) = [Pair] -> Value
object
    [ Key
"kvar" Key -> KVar -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= KVar
k
    , Key
"val"  Key -> a -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= a
v
    ]

instance ToJSON a => ToJSON (KVarMap a) where
  toJSON :: KVarMap a -> Value
toJSON = [KVarBind a] -> Value
forall a. ToJSON a => a -> Value
toJSON ([KVarBind a] -> Value)
-> (KVarMap a -> [KVarBind a]) -> KVarMap a -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((KVar, a) -> KVarBind a) -> [(KVar, a)] -> [KVarBind a]
forall a b. (a -> b) -> [a] -> [b]
map (KVar, a) -> KVarBind a
forall a. (KVar, a) -> KVarBind a
MkKVarBind ([(KVar, a)] -> [KVarBind a])
-> (KVarMap a -> [(KVar, a)]) -> KVarMap a -> [KVarBind a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap KVar a -> [(KVar, a)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap KVar a -> [(KVar, a)])
-> (KVarMap a -> HashMap KVar a) -> KVarMap a -> [(KVar, a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KVarMap a -> HashMap KVar a
forall a. KVarMap a -> HashMap KVar a
unKVarMap

instance ToJSON ScopedExpr where
  toJSON :: ScopedExpr -> Value
toJSON = [Char] -> Value
forall a. ToJSON a => a -> Value
toJSON ([Char] -> Value) -> (ScopedExpr -> [Char]) -> ScopedExpr -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Char]
render (Doc -> [Char]) -> (ScopedExpr -> Doc) -> ScopedExpr -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopedExpr -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT

instance Semigroup (Result a) where
  Result a
r1 <> :: Result a -> Result a -> Result a
<> Result a
r2  = FixResult a
-> FixSolution -> FixDelayedSolution -> ResultSorts -> Result a
forall a.
FixResult a
-> FixSolution -> FixDelayedSolution -> ResultSorts -> Result a
Result FixResult a
stat FixSolution
soln FixDelayedSolution
nonCutsSoln ResultSorts
sorts
    where
      stat :: FixResult a
stat  = Result a -> FixResult a
forall a. Result a -> FixResult a
resStatus Result a
r1    FixResult a -> FixResult a -> FixResult a
forall a. Semigroup a => a -> a -> a
<> Result a -> FixResult a
forall a. Result a -> FixResult a
resStatus Result a
r2
      soln :: FixSolution
soln  = Result a -> FixSolution
forall a. Result a -> FixSolution
resSolution Result a
r1  FixSolution -> FixSolution -> FixSolution
forall a. Semigroup a => a -> a -> a
<> Result a -> FixSolution
forall a. Result a -> FixSolution
resSolution Result a
r2
      nonCutsSoln :: FixDelayedSolution
nonCutsSoln = Result a -> FixDelayedSolution
forall a. Result a -> FixDelayedSolution
resNonCutsSolution Result a
r1 FixDelayedSolution -> FixDelayedSolution -> FixDelayedSolution
forall a. Semigroup a => a -> a -> a
<> Result a -> FixDelayedSolution
forall a. Result a -> FixDelayedSolution
resNonCutsSolution Result a
r2
      sorts :: ResultSorts
sorts = ([(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)])
-> ResultSorts -> ResultSorts -> ResultSorts
forall k v.
Eq k =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
M.unionWith [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. Eq a => [a] -> [a] -> [a]
L.union (Result a -> ResultSorts
forall a. Result a -> ResultSorts
resSorts Result a
r1) (Result a -> ResultSorts
forall a. Result a -> ResultSorts
resSorts Result a
r2)

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

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

isSafe :: Result a -> Bool
isSafe :: forall a. Result a -> Bool
isSafe Result a
r = case Result a -> FixResult a
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]
_ <- Result a -> FixResult 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 (BindId -> [Char]
forall a. Show a => a -> [Char]
show (BindId -> [Char]) -> BindId -> [Char]
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 ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [ [Char] -> Doc
text [Char]
"Crash!" ] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++  [Char] -> [SubC a] -> [Doc]
forall a. (Ord a, Fixpoint a) => [Char] -> [SubC a] -> [Doc]
pprSinfos [Char]
"CRASH: " ((SubC a, Maybe [Char]) -> SubC a
forall a b. (a, b) -> a
fst ((SubC a, Maybe [Char]) -> SubC a)
-> [(SubC a, Maybe [Char])] -> [SubC a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SubC a, Maybe [Char])]
xs) [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> Doc
parens ([Char] -> Doc
text [Char]
msg)]
  toFix (Unsafe Stats
_ [SubC a]
xs)    = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
text [Char]
"Unsafe:" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Char] -> [SubC a] -> [Doc]
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 = (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (([Char] -> Doc
text [Char]
msg Doc -> Doc -> Doc
<->) (Doc -> Doc) -> (a -> Doc) -> a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
forall a. Fixpoint a => a -> Doc
toFix) ([a] -> [Doc]) -> ([SubC a] -> [a]) -> [SubC a] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [a]
forall a. Ord a => [a] -> [a]
L.sort ([a] -> [a]) -> ([SubC a] -> [a]) -> [SubC a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SubC a -> a) -> [SubC a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SubC a -> a
forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo

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

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

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

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

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

instance Fixpoint a => PPrint (WfC a) where
  pprintTidy :: Tidy -> WfC a -> Doc
pprintTidy Tidy
_ = WfC a -> Doc
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 =   IBindEnv -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SubC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
c)
              Doc -> Doc -> Doc
$+$ [Char] -> Doc
text [Char]
"lhs" Doc -> Doc -> Doc
<+> SortedReft -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
c)
              Doc -> Doc -> Doc
$+$ [Char] -> Doc
text [Char]
"rhs" Doc -> Doc -> Doc
<+> SortedReft -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs SubC a
c)
              Doc -> Doc -> Doc
$+$ (Maybe Integer -> Doc
forall a. Show a => Maybe a -> Doc
pprId (SubC a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
sid SubC a
c) Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"tag" Doc -> Doc -> Doc
<+> Tag -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SubC a -> Tag
forall (c :: * -> *) a. TaggedC c a => c a -> Tag
stag SubC a
c))
              Doc -> Doc -> Doc
$+$ Doc -> Doc -> Doc
toFixMeta ([Char] -> Doc
text [Char]
"constraint" Doc -> Doc -> Doc
<+> Maybe Integer -> Doc
forall a. Show a => Maybe a -> Doc
pprId (SubC a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
sid SubC a
c)) (a -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SubC a -> a
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 =   IBindEnv -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC a
c)
              Doc -> Doc -> Doc
$+$ [Char] -> Doc
text [Char]
"rhs" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SimpC a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
crhs SimpC a
c)
              Doc -> Doc -> Doc
$+$ (Maybe Integer -> Doc
forall a. Show a => Maybe a -> Doc
pprId (SimpC a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
sid SimpC a
c) Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"tag" Doc -> Doc -> Doc
<+> Tag -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SimpC a -> Tag
forall (c :: * -> *) a. TaggedC c a => c a -> Tag
stag SimpC a
c))
              Doc -> Doc -> Doc
$+$ Doc -> Doc -> Doc
toFixMeta ([Char] -> Doc
text [Char]
"simpleConstraint" Doc -> Doc -> Doc
<+> Maybe Integer -> Doc
forall a. Show a => Maybe a -> Doc
pprId (SimpC a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
sid SimpC a
c)) (a -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SimpC a -> a
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  =   IBindEnv -> Doc
forall a. Fixpoint a => a -> Doc
toFix (WfC a -> IBindEnv
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
<+> SortedReft -> Doc
forall a. Fixpoint a => a -> Doc
toFix (Sort -> ReftV Symbol -> SortedReft
RR Sort
t ((Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
v, KVar -> SubstV Symbol -> Expr
forall v. KVar -> SubstV v -> ExprV v
PKVar KVar
k SubstV Symbol
forall a. Monoid a => a
mempty)))
              Doc -> Doc -> Doc
$+$ Doc -> Doc -> Doc
toFixMeta ([Char] -> Doc
text [Char]
"wf") (a -> Doc
forall a. Fixpoint a => a -> Doc
toFix (WfC a -> a
forall a. WfC a -> a
winfo WfC a
w))
          (Symbol
v, Sort
t, KVar
k) = WfC a -> (Symbol, Sort, KVar)
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
<+> a -> Doc
forall a. Show a => a -> Doc
tshow a
i
pprId Maybe a
_         = Doc
""

----------------------------------------------------------------
instance S.Store QualPattern
instance S.Store QualParam
instance S.Store Qualifier
instance S.Store Kuts
instance S.Store HOInfo
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 v => NFData (QualifierV v)
instance NFData Kuts
instance NFData HOInfo

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 v => Hashable (QualifierV v)
instance Hashable QualPattern
instance Hashable QualParam
instance Hashable v => Hashable (EquationV v)

instance B.Binary QualPattern
instance B.Binary QualParam
instance B.Binary v => B.Binary (QualifierV v)
instance B.Binary v => B.Binary (EquationV v)

---------------------------------------------------------------------------
-- | "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 (SubstV Symbol -> Bool) -> [SubstV Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SubstV Symbol -> Bool
isEmptySubst [SubstV Symbol]
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 [IBindEnv -> (Symbol, Sort, KVar) -> a -> WfC a
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 ]
                else [Char] -> [WfC a]
forall a. (?callStack::CallStack) => [Char] -> a
errorstar [Char]
msg
  where
    msg :: [Char]
msg             = [Char]
"wfKvar: malformed wfC " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SortedReft -> [Char]
forall a. Show a => a -> [Char]
show SortedReft
sr [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [SubstV Symbol] -> [Char]
forall a. Show a => a -> [Char]
show [SubstV Symbol]
sus
    Reft (Symbol
v, Expr
ras)   = SortedReft -> ReftV Symbol
sr_reft SortedReft
sr
    ([KVar]
ks, [SubstV Symbol]
sus)       = [(KVar, SubstV Symbol)] -> ([KVar], [SubstV Symbol])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(KVar, SubstV Symbol)] -> ([KVar], [SubstV Symbol]))
-> [(KVar, SubstV Symbol)] -> ([KVar], [SubstV Symbol])
forall a b. (a -> b) -> a -> b
$ Expr -> [(KVar, SubstV Symbol)]
forall {v}. ExprV v -> [(KVar, SubstV v)]
go Expr
ras

    go :: ExprV v -> [(KVar, SubstV v)]
go (PKVar KVar
k SubstV v
su) = [(KVar
k, SubstV v
su)]
    go (PAnd [ExprV v]
es)    = [(KVar
k, SubstV v
su) | PKVar KVar
k SubstV v
su <- [ExprV v]
es]
    go ExprV v
_            = []

mkSubC :: IBindEnv -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a
mkSubC :: forall a.
IBindEnv
-> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a
mkSubC = IBindEnv
-> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a
forall a.
IBindEnv
-> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a
SubC

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

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

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

addIds :: [SubC a] -> [(Integer, SubC a)]
addIds :: forall a. [SubC a] -> [(Integer, SubC a)]
addIds = (Integer -> SubC a -> (Integer, SubC a))
-> [Integer] -> [SubC a] -> [(Integer, SubC a)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Integer
i SubC a
c -> (Integer
i, Integer -> SubC a -> SubC a
forall {a} {a}. Show a => a -> SubC a -> SubC a
shiftId Integer
i (SubC a -> SubC a) -> SubC a -> SubC a
forall a b. (a -> b) -> a -> b
$ SubC a
c {_sid = Just i})) [Integer
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 = shiftSR i (slhs c) }
                    { srhs = shiftSR i (srhs c) }
    shiftSR :: a -> SortedReft -> SortedReft
shiftSR a
i SortedReft
sr = SortedReft
sr { sr_reft = shiftR i $ sr_reft sr }
    shiftR :: a -> ReftV Symbol -> ReftV Symbol
shiftR a
i r :: ReftV Symbol
r@(Reft (Symbol
v, Expr
_)) = ReftV Symbol -> Symbol -> ReftV Symbol
shiftVV ReftV Symbol
r (Symbol -> a -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
v a
i)

--------------------------------------------------------------------------------
-- | Qualifiers ----------------------------------------------------------------
--------------------------------------------------------------------------------
type Qualifier = QualifierV Symbol
data QualifierV v = Q
  { forall v. QualifierV v -> Symbol
qName   :: !Symbol     -- ^ Name
  , forall v. QualifierV v -> [QualParam]
qParams :: [QualParam] -- ^ Parameters
  , forall v. QualifierV v -> ExprV v
qBody   :: !(ExprV v)  -- ^ Predicate
  , forall v. QualifierV v -> SourcePos
qPos    :: !SourcePos  -- ^ Source Location
  }
  deriving (QualifierV v -> QualifierV v -> Bool
(QualifierV v -> QualifierV v -> Bool)
-> (QualifierV v -> QualifierV v -> Bool) -> Eq (QualifierV v)
forall v. Eq v => QualifierV v -> QualifierV v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall v. Eq v => QualifierV v -> QualifierV v -> Bool
== :: QualifierV v -> QualifierV v -> Bool
$c/= :: forall v. Eq v => QualifierV v -> QualifierV v -> Bool
/= :: QualifierV v -> QualifierV v -> Bool
Eq, Eq (QualifierV v)
Eq (QualifierV v) =>
(QualifierV v -> QualifierV v -> Ordering)
-> (QualifierV v -> QualifierV v -> Bool)
-> (QualifierV v -> QualifierV v -> Bool)
-> (QualifierV v -> QualifierV v -> Bool)
-> (QualifierV v -> QualifierV v -> Bool)
-> (QualifierV v -> QualifierV v -> QualifierV v)
-> (QualifierV v -> QualifierV v -> QualifierV v)
-> Ord (QualifierV v)
QualifierV v -> QualifierV v -> Bool
QualifierV v -> QualifierV v -> Ordering
QualifierV v -> QualifierV v -> QualifierV v
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
forall v. Ord v => Eq (QualifierV v)
forall v. Ord v => QualifierV v -> QualifierV v -> Bool
forall v. Ord v => QualifierV v -> QualifierV v -> Ordering
forall v. Ord v => QualifierV v -> QualifierV v -> QualifierV v
$ccompare :: forall v. Ord v => QualifierV v -> QualifierV v -> Ordering
compare :: QualifierV v -> QualifierV v -> Ordering
$c< :: forall v. Ord v => QualifierV v -> QualifierV v -> Bool
< :: QualifierV v -> QualifierV v -> Bool
$c<= :: forall v. Ord v => QualifierV v -> QualifierV v -> Bool
<= :: QualifierV v -> QualifierV v -> Bool
$c> :: forall v. Ord v => QualifierV v -> QualifierV v -> Bool
> :: QualifierV v -> QualifierV v -> Bool
$c>= :: forall v. Ord v => QualifierV v -> QualifierV v -> Bool
>= :: QualifierV v -> QualifierV v -> Bool
$cmax :: forall v. Ord v => QualifierV v -> QualifierV v -> QualifierV v
max :: QualifierV v -> QualifierV v -> QualifierV v
$cmin :: forall v. Ord v => QualifierV v -> QualifierV v -> QualifierV v
min :: QualifierV v -> QualifierV v -> QualifierV v
Ord, BindId -> QualifierV v -> [Char] -> [Char]
[QualifierV v] -> [Char] -> [Char]
QualifierV v -> [Char]
(BindId -> QualifierV v -> [Char] -> [Char])
-> (QualifierV v -> [Char])
-> ([QualifierV v] -> [Char] -> [Char])
-> Show (QualifierV v)
forall v.
(Show v, Fixpoint v, Ord v) =>
BindId -> QualifierV v -> [Char] -> [Char]
forall v.
(Show v, Fixpoint v, Ord v) =>
[QualifierV v] -> [Char] -> [Char]
forall v. (Show v, Fixpoint v, Ord v) => QualifierV v -> [Char]
forall a.
(BindId -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: forall v.
(Show v, Fixpoint v, Ord v) =>
BindId -> QualifierV v -> [Char] -> [Char]
showsPrec :: BindId -> QualifierV v -> [Char] -> [Char]
$cshow :: forall v. (Show v, Fixpoint v, Ord v) => QualifierV v -> [Char]
show :: QualifierV v -> [Char]
$cshowList :: forall v.
(Show v, Fixpoint v, Ord v) =>
[QualifierV v] -> [Char] -> [Char]
showList :: [QualifierV v] -> [Char] -> [Char]
Show, Typeable (QualifierV v)
Typeable (QualifierV v) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> QualifierV v -> c (QualifierV v))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (QualifierV v))
-> (QualifierV v -> Constr)
-> (QualifierV v -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (QualifierV v)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (QualifierV v)))
-> ((forall b. Data b => b -> b) -> QualifierV v -> QualifierV v)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> QualifierV v -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> QualifierV v -> r)
-> (forall u. (forall d. Data d => d -> u) -> QualifierV v -> [u])
-> (forall u.
    BindId -> (forall d. Data d => d -> u) -> QualifierV v -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> QualifierV v -> m (QualifierV v))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QualifierV v -> m (QualifierV v))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QualifierV v -> m (QualifierV v))
-> Data (QualifierV v)
QualifierV v -> Constr
QualifierV v -> DataType
(forall b. Data b => b -> b) -> QualifierV v -> QualifierV v
forall v. Data v => Typeable (QualifierV v)
forall v. Data v => QualifierV v -> Constr
forall v. Data v => QualifierV v -> DataType
forall v.
Data v =>
(forall b. Data b => b -> b) -> QualifierV v -> QualifierV v
forall v u.
Data v =>
BindId -> (forall d. Data d => d -> u) -> QualifierV v -> u
forall v u.
Data v =>
(forall d. Data d => d -> u) -> QualifierV v -> [u]
forall v r r'.
Data v =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualifierV v -> r
forall v r r'.
Data v =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualifierV v -> r
forall v (m :: * -> *).
(Data v, Monad m) =>
(forall d. Data d => d -> m d) -> QualifierV v -> m (QualifierV v)
forall v (m :: * -> *).
(Data v, MonadPlus m) =>
(forall d. Data d => d -> m d) -> QualifierV v -> m (QualifierV v)
forall v (c :: * -> *).
Data v =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (QualifierV v)
forall v (c :: * -> *).
Data v =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualifierV v -> c (QualifierV v)
forall v (t :: * -> *) (c :: * -> *).
(Data v, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (QualifierV v))
forall v (t :: * -> * -> *) (c :: * -> *).
(Data v, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (QualifierV v))
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) -> QualifierV v -> u
forall u. (forall d. Data d => d -> u) -> QualifierV v -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualifierV v -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualifierV v -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QualifierV v -> m (QualifierV v)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualifierV v -> m (QualifierV v)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (QualifierV v)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualifierV v -> c (QualifierV v)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (QualifierV v))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (QualifierV v))
$cgfoldl :: forall v (c :: * -> *).
Data v =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualifierV v -> c (QualifierV v)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualifierV v -> c (QualifierV v)
$cgunfold :: forall v (c :: * -> *).
Data v =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (QualifierV v)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (QualifierV v)
$ctoConstr :: forall v. Data v => QualifierV v -> Constr
toConstr :: QualifierV v -> Constr
$cdataTypeOf :: forall v. Data v => QualifierV v -> DataType
dataTypeOf :: QualifierV v -> DataType
$cdataCast1 :: forall v (t :: * -> *) (c :: * -> *).
(Data v, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (QualifierV v))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (QualifierV v))
$cdataCast2 :: forall v (t :: * -> * -> *) (c :: * -> *).
(Data v, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (QualifierV v))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (QualifierV v))
$cgmapT :: forall v.
Data v =>
(forall b. Data b => b -> b) -> QualifierV v -> QualifierV v
gmapT :: (forall b. Data b => b -> b) -> QualifierV v -> QualifierV v
$cgmapQl :: forall v r r'.
Data v =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualifierV v -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualifierV v -> r
$cgmapQr :: forall v r r'.
Data v =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualifierV v -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualifierV v -> r
$cgmapQ :: forall v u.
Data v =>
(forall d. Data d => d -> u) -> QualifierV v -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> QualifierV v -> [u]
$cgmapQi :: forall v u.
Data v =>
BindId -> (forall d. Data d => d -> u) -> QualifierV v -> u
gmapQi :: forall u.
BindId -> (forall d. Data d => d -> u) -> QualifierV v -> u
$cgmapM :: forall v (m :: * -> *).
(Data v, Monad m) =>
(forall d. Data d => d -> m d) -> QualifierV v -> m (QualifierV v)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QualifierV v -> m (QualifierV v)
$cgmapMp :: forall v (m :: * -> *).
(Data v, MonadPlus m) =>
(forall d. Data d => d -> m d) -> QualifierV v -> m (QualifierV v)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualifierV v -> m (QualifierV v)
$cgmapMo :: forall v (m :: * -> *).
(Data v, MonadPlus m) =>
(forall d. Data d => d -> m d) -> QualifierV v -> m (QualifierV v)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualifierV v -> m (QualifierV v)
Data, Typeable, (forall x. QualifierV v -> Rep (QualifierV v) x)
-> (forall x. Rep (QualifierV v) x -> QualifierV v)
-> Generic (QualifierV v)
forall x. Rep (QualifierV v) x -> QualifierV v
forall x. QualifierV v -> Rep (QualifierV v) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall v x. Rep (QualifierV v) x -> QualifierV v
forall v x. QualifierV v -> Rep (QualifierV v) x
$cfrom :: forall v x. QualifierV v -> Rep (QualifierV v) x
from :: forall x. QualifierV v -> Rep (QualifierV v) x
$cto :: forall v x. Rep (QualifierV v) x -> QualifierV v
to :: forall x. Rep (QualifierV v) x -> QualifierV v
Generic, (forall a b. (a -> b) -> QualifierV a -> QualifierV b)
-> (forall a b. a -> QualifierV b -> QualifierV a)
-> Functor QualifierV
forall a b. a -> QualifierV b -> QualifierV a
forall a b. (a -> b) -> QualifierV a -> QualifierV b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> QualifierV a -> QualifierV b
fmap :: forall a b. (a -> b) -> QualifierV a -> QualifierV b
$c<$ :: forall a b. a -> QualifierV b -> QualifierV a
<$ :: forall a b. a -> QualifierV b -> QualifierV a
Functor, (forall m. Monoid m => QualifierV m -> m)
-> (forall m a. Monoid m => (a -> m) -> QualifierV a -> m)
-> (forall m a. Monoid m => (a -> m) -> QualifierV a -> m)
-> (forall a b. (a -> b -> b) -> b -> QualifierV a -> b)
-> (forall a b. (a -> b -> b) -> b -> QualifierV a -> b)
-> (forall b a. (b -> a -> b) -> b -> QualifierV a -> b)
-> (forall b a. (b -> a -> b) -> b -> QualifierV a -> b)
-> (forall a. (a -> a -> a) -> QualifierV a -> a)
-> (forall a. (a -> a -> a) -> QualifierV a -> a)
-> (forall a. QualifierV a -> [a])
-> (forall a. QualifierV a -> Bool)
-> (forall a. QualifierV a -> BindId)
-> (forall a. Eq a => a -> QualifierV a -> Bool)
-> (forall a. Ord a => QualifierV a -> a)
-> (forall a. Ord a => QualifierV a -> a)
-> (forall a. Num a => QualifierV a -> a)
-> (forall a. Num a => QualifierV a -> a)
-> Foldable QualifierV
forall a. Eq a => a -> QualifierV a -> Bool
forall a. Num a => QualifierV a -> a
forall a. Ord a => QualifierV a -> a
forall m. Monoid m => QualifierV m -> m
forall a. QualifierV a -> Bool
forall a. QualifierV a -> BindId
forall a. QualifierV a -> [a]
forall a. (a -> a -> a) -> QualifierV a -> a
forall m a. Monoid m => (a -> m) -> QualifierV a -> m
forall b a. (b -> a -> b) -> b -> QualifierV a -> b
forall a b. (a -> b -> b) -> b -> QualifierV a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> BindId)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => QualifierV m -> m
fold :: forall m. Monoid m => QualifierV m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> QualifierV a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> QualifierV a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> QualifierV a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> QualifierV a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> QualifierV a -> b
foldr :: forall a b. (a -> b -> b) -> b -> QualifierV a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> QualifierV a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> QualifierV a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> QualifierV a -> b
foldl :: forall b a. (b -> a -> b) -> b -> QualifierV a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> QualifierV a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> QualifierV a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> QualifierV a -> a
foldr1 :: forall a. (a -> a -> a) -> QualifierV a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> QualifierV a -> a
foldl1 :: forall a. (a -> a -> a) -> QualifierV a -> a
$ctoList :: forall a. QualifierV a -> [a]
toList :: forall a. QualifierV a -> [a]
$cnull :: forall a. QualifierV a -> Bool
null :: forall a. QualifierV a -> Bool
$clength :: forall a. QualifierV a -> BindId
length :: forall a. QualifierV a -> BindId
$celem :: forall a. Eq a => a -> QualifierV a -> Bool
elem :: forall a. Eq a => a -> QualifierV a -> Bool
$cmaximum :: forall a. Ord a => QualifierV a -> a
maximum :: forall a. Ord a => QualifierV a -> a
$cminimum :: forall a. Ord a => QualifierV a -> a
minimum :: forall a. Ord a => QualifierV a -> a
$csum :: forall a. Num a => QualifierV a -> a
sum :: forall a. Num a => QualifierV a -> a
$cproduct :: forall a. Num a => QualifierV a -> a
product :: forall a. Num a => QualifierV a -> a
Foldable, Functor QualifierV
Foldable QualifierV
(Functor QualifierV, Foldable QualifierV) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> QualifierV a -> f (QualifierV b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    QualifierV (f a) -> f (QualifierV a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> QualifierV a -> m (QualifierV b))
-> (forall (m :: * -> *) a.
    Monad m =>
    QualifierV (m a) -> m (QualifierV a))
-> Traversable QualifierV
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
QualifierV (m a) -> m (QualifierV a)
forall (f :: * -> *) a.
Applicative f =>
QualifierV (f a) -> f (QualifierV a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> QualifierV a -> m (QualifierV b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> QualifierV a -> f (QualifierV b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> QualifierV a -> f (QualifierV b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> QualifierV a -> f (QualifierV b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
QualifierV (f a) -> f (QualifierV a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
QualifierV (f a) -> f (QualifierV a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> QualifierV a -> m (QualifierV b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> QualifierV a -> m (QualifierV b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
QualifierV (m a) -> m (QualifierV a)
sequence :: forall (m :: * -> *) a.
Monad m =>
QualifierV (m a) -> m (QualifierV a)
Traversable)

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

instance ToHornSMT QualParam where
  toHornSMT :: QualParam -> Doc
toHornSMT QualParam
qp = (Symbol, Sort) -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (QualParam -> Symbol
qpSym QualParam
qp, QualParam -> Sort
qpSort QualParam
qp)


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
(QualPattern -> QualPattern -> Bool)
-> (QualPattern -> QualPattern -> Bool) -> Eq QualPattern
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: QualPattern -> QualPattern -> Bool
== :: QualPattern -> QualPattern -> Bool
$c/= :: QualPattern -> QualPattern -> Bool
/= :: QualPattern -> QualPattern -> Bool
Eq, Eq QualPattern
Eq QualPattern =>
(QualPattern -> QualPattern -> Ordering)
-> (QualPattern -> QualPattern -> Bool)
-> (QualPattern -> QualPattern -> Bool)
-> (QualPattern -> QualPattern -> Bool)
-> (QualPattern -> QualPattern -> Bool)
-> (QualPattern -> QualPattern -> QualPattern)
-> (QualPattern -> QualPattern -> QualPattern)
-> Ord 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
$ccompare :: QualPattern -> QualPattern -> Ordering
compare :: QualPattern -> QualPattern -> Ordering
$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
>= :: QualPattern -> QualPattern -> Bool
$cmax :: QualPattern -> QualPattern -> QualPattern
max :: QualPattern -> QualPattern -> QualPattern
$cmin :: QualPattern -> QualPattern -> QualPattern
min :: QualPattern -> QualPattern -> QualPattern
Ord, BindId -> QualPattern -> [Char] -> [Char]
[QualPattern] -> [Char] -> [Char]
QualPattern -> [Char]
(BindId -> QualPattern -> [Char] -> [Char])
-> (QualPattern -> [Char])
-> ([QualPattern] -> [Char] -> [Char])
-> Show QualPattern
forall a.
(BindId -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: BindId -> QualPattern -> [Char] -> [Char]
showsPrec :: BindId -> QualPattern -> [Char] -> [Char]
$cshow :: QualPattern -> [Char]
show :: QualPattern -> [Char]
$cshowList :: [QualPattern] -> [Char] -> [Char]
showList :: [QualPattern] -> [Char] -> [Char]
Show, Typeable QualPattern
Typeable QualPattern =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> QualPattern -> c QualPattern)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c QualPattern)
-> (QualPattern -> Constr)
-> (QualPattern -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> QualPattern -> QualPattern)
-> (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 u. (forall d. Data d => d -> u) -> QualPattern -> [u])
-> (forall u.
    BindId -> (forall d. Data d => d -> u) -> QualPattern -> u)
-> (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 (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QualPattern -> m QualPattern)
-> Data QualPattern
QualPattern -> Constr
QualPattern -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualPattern -> c QualPattern
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualPattern -> c QualPattern
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QualPattern
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QualPattern
$ctoConstr :: QualPattern -> Constr
toConstr :: QualPattern -> Constr
$cdataTypeOf :: QualPattern -> DataType
dataTypeOf :: QualPattern -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QualPattern)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QualPattern)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c QualPattern)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c QualPattern)
$cgmapT :: (forall b. Data b => b -> b) -> QualPattern -> QualPattern
gmapT :: (forall b. Data b => b -> b) -> QualPattern -> QualPattern
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualPattern -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualPattern -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> QualPattern -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> QualPattern -> [u]
$cgmapQi :: forall u.
BindId -> (forall d. Data d => d -> u) -> QualPattern -> u
gmapQi :: forall u.
BindId -> (forall d. Data d => d -> u) -> QualPattern -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
Data, Typeable, (forall x. QualPattern -> Rep QualPattern x)
-> (forall x. Rep QualPattern x -> QualPattern)
-> Generic QualPattern
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
$cfrom :: forall x. QualPattern -> Rep QualPattern x
from :: forall x. QualPattern -> Rep QualPattern x
$cto :: forall x. Rep QualPattern x -> QualPattern
to :: forall x. Rep QualPattern x -> QualPattern
Generic)

instance ToJSON   Qualifier   where
instance FromJSON Qualifier   where
instance ToJSON   QualParam   where
instance FromJSON QualParam   where
instance ToJSON   QualPattern where
instance FromJSON QualPattern where
instance ToJSON   Equation    where
instance FromJSON Equation    where
instance ToJSON   Rewrite     where
instance FromJSON Rewrite     where

instance ToHornSMT Qualifier where
  toHornSMT :: Qualifier -> Doc
toHornSMT (Q Symbol
n [QualParam]
qps Expr
p SourcePos
_) =  Doc -> [(Symbol, Sort)] -> Expr -> Doc
forall a t.
(ToHornSMT a, ToHornSMT t) =>
Doc -> [(Symbol, t)] -> a -> Doc
toHornWithBinders Doc
name [(Symbol, Sort)]
xts Expr
p
    where
      name :: Doc
name = Doc
"qualif" Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
n
      xts :: [(Symbol, Sort)]
xts =  [(QualParam -> Symbol
qpSym QualParam
qp, QualParam -> Sort
qpSort QualParam
qp) | QualParam
qp <- [QualParam]
qps]

trueQual :: Qualifier
trueQual :: Qualifier
trueQual = Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
forall v.
Symbol -> [QualParam] -> ExprV v -> SourcePos -> QualifierV v
Q ([Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol ([Char]
"QTrue" :: String)) [] Expr
forall v. ExprV v
PTrue ([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
forall v. QualifierV v -> SourcePos
qPos Qualifier
q

instance Subable Qualifier where
  syms :: Qualifier -> [Symbol]
syms   = Qualifier -> [Symbol]
qualFreeSymbols
  subst :: (?callStack::CallStack) => SubstV Symbol -> Qualifier -> Qualifier
subst  = (Expr -> Expr) -> Qualifier -> Qualifier
mapQualBody ((Expr -> Expr) -> Qualifier -> Qualifier)
-> (SubstV Symbol -> Expr -> Expr)
-> SubstV Symbol
-> Qualifier
-> Qualifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubstV Symbol -> Expr -> Expr
forall a.
(Subable a, ?callStack::CallStack) =>
SubstV Symbol -> a -> a
subst
  substf :: (Symbol -> Expr) -> Qualifier -> Qualifier
substf = (Expr -> Expr) -> Qualifier -> Qualifier
mapQualBody ((Expr -> Expr) -> Qualifier -> Qualifier)
-> ((Symbol -> Expr) -> Expr -> Expr)
-> (Symbol -> Expr)
-> Qualifier
-> Qualifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Expr) -> Expr -> Expr
forall a. Subable a => (Symbol -> Expr) -> a -> a
substf
  substa :: (Symbol -> Symbol) -> Qualifier -> Qualifier
substa = (Expr -> Expr) -> Qualifier -> Qualifier
mapQualBody ((Expr -> Expr) -> Qualifier -> Qualifier)
-> ((Symbol -> Symbol) -> Expr -> Expr)
-> (Symbol -> Symbol)
-> Qualifier
-> Qualifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Symbol) -> Expr -> Expr
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 = f (qBody q) }

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

instance Fixpoint QualParam where
  toFix :: QualParam -> Doc
toFix (QP Symbol
x QualPattern
_ Sort
t) = (Symbol, Sort) -> Doc
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) = Tidy -> Symbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
x Doc -> Doc -> Doc
<+> Tidy -> QualPattern -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k QualPattern
pat Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> Tidy -> Sort -> 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
<+> Tidy -> Symbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
s Doc -> Doc -> Doc
<+> (Doc
"$" Doc -> Doc -> Doc
<-> BindId -> 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
<-> Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
i) Doc -> Doc -> Doc
<+> Tidy -> BindId -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k BindId
s
  pprintTidy Tidy
k (PatExact  Symbol
s  ) = Doc
"~"  Doc -> Doc -> Doc
<+> Tidy -> Symbol -> 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 (Ord v, Fixpoint v, PPrint v) => PPrint (QualifierV v) where
  pprintTidy :: Tidy -> QualifierV v -> Doc
pprintTidy Tidy
k QualifierV v
q =
    Doc
"qualif" Doc -> Doc -> Doc
<+> Tidy -> Symbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (QualifierV v -> Symbol
forall v. QualifierV v -> Symbol
qName QualifierV v
q) Doc -> Doc -> Doc
<+>
     Doc -> Doc
parens ([Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma (Tidy -> QualParam -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (QualParam -> Doc) -> [QualParam] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QualifierV v -> [QualParam]
forall v. QualifierV v -> [QualParam]
qParams QualifierV v
q)) Doc -> Doc -> Doc
<+>
     Doc -> Doc
braces (Tidy -> ExprV v -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (QualifierV v -> ExprV v
forall v. QualifierV v -> ExprV v
qBody QualifierV v
q)) Doc -> Doc -> Doc
<+> Doc
"//defined at" Doc -> Doc -> Doc
<+> Tidy -> SourcePos -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (QualifierV v -> SourcePos
forall v. QualifierV v -> SourcePos
qPos QualifierV v
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 -> Doc
braces (Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix Expr
p) Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"//" Doc -> Doc -> Doc
<+> SourcePos -> Doc
forall a. Fixpoint a => a -> Doc
toFix SourcePos
l
  where
    args :: Doc
args              = Doc -> [Doc] -> Doc
intersperse Doc
comma (QualParam -> Doc
forall a. Fixpoint a => a -> Doc
toFix (QualParam -> Doc) -> [QualParam] -> [Doc]
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) (Symbol, Sort) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. a -> [a] -> [a]
: [(Symbol, Sort)]
xts) Expr
p SourcePos
l
  where
    xs :: [Symbol]
xs  = Symbol -> [Symbol] -> [Symbol]
forall a. Eq a => a -> [a] -> [a]
L.delete Symbol
v ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a]
L.nub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms Expr
p
    xts :: [(Symbol, Sort)]
xts = [Maybe (Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Symbol, Sort)] -> [(Symbol, Sort)])
-> [Maybe (Symbol, Sort)] -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ (Symbol -> Integer -> Maybe (Symbol, Sort))
-> [Symbol] -> [Integer] -> [Maybe (Symbol, Sort)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (SourcePos
-> SEnv Sort
-> SEnv Sort
-> Symbol
-> Integer
-> Maybe (Symbol, Sort)
envSort SourcePos
l SEnv Sort
lEnv SEnv Sort
γ) [Symbol]
xs [Integer
0..]

mkQ :: Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier
mkQ :: Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier
mkQ Symbol
n = Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
forall v.
Symbol -> [QualParam] -> ExprV v -> SourcePos -> QualifierV v
Q Symbol
n ([QualParam] -> Expr -> SourcePos -> Qualifier)
-> ([(Symbol, Sort)] -> [QualParam])
-> [(Symbol, Sort)]
-> Expr
-> SourcePos
-> Qualifier
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]
forall v. QualifierV v -> [QualParam]
qParams Qualifier
q ]

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

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

-- | constructing qualifiers
mkQual :: Symbol -> [QualParam] -> ExprV v -> SourcePos -> QualifierV v
mkQual :: forall v.
Symbol -> [QualParam] -> ExprV v -> SourcePos -> QualifierV v
mkQual Symbol
n [QualParam]
qps ExprV v
p = Symbol -> [QualParam] -> ExprV v -> SourcePos -> QualifierV v
forall v.
Symbol -> [QualParam] -> ExprV v -> SourcePos -> QualifierV v
Q Symbol
n [QualParam]
qps' ExprV v
p
  where
    qps' :: [QualParam]
qps'       = (QualParam -> Sort -> QualParam)
-> [QualParam] -> [Sort] -> [QualParam]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\QualParam
qp Sort
t' -> QualParam
qp { qpSort = t'}) [QualParam]
qps [Sort]
ts'
    ts' :: [Sort]
ts'        = [Sort] -> [Sort]
gSorts (QualParam -> Sort
qpSort (QualParam -> Sort) -> [QualParam] -> [Sort]
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 (Sort -> Sort) -> [Sort] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
ts
  where
    su :: [(Symbol, BindId)]
su    = ([Symbol] -> Tag -> [(Symbol, BindId)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [BindId
0..]) ([Symbol] -> [(Symbol, BindId)])
-> ([Sort] -> [Symbol]) -> [Sort] -> [(Symbol, BindId)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol] -> [Symbol]
forall a. Ord a => [a] -> [a]
sortNub ([Symbol] -> [Symbol])
-> ([Sort] -> [Symbol]) -> [Sort] -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort -> [Symbol]) -> [Sort] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Sort -> [Symbol]
sortVars ([Sort] -> [(Symbol, BindId)]) -> [Sort] -> [(Symbol, BindId)]
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 <- Symbol -> [(Symbol, BindId)] -> Maybe BindId
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 = ([Symbol] -> Sort -> [Symbol]) -> [Symbol] -> Sort -> [Symbol]
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 Symbol -> [Symbol] -> [Symbol]
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 (Sort -> Sort) -> (Sort -> Sort) -> Sort -> Sort
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) = (a -> Sort -> a) -> a -> [Sort] -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
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)  = (a -> Sort -> a) -> a -> [Sort] -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
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
(Kuts -> Kuts -> Bool) -> (Kuts -> Kuts -> Bool) -> Eq Kuts
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Kuts -> Kuts -> Bool
== :: Kuts -> Kuts -> Bool
$c/= :: Kuts -> Kuts -> Bool
/= :: Kuts -> Kuts -> Bool
Eq, BindId -> Kuts -> [Char] -> [Char]
[Kuts] -> [Char] -> [Char]
Kuts -> [Char]
(BindId -> Kuts -> [Char] -> [Char])
-> (Kuts -> [Char]) -> ([Kuts] -> [Char] -> [Char]) -> Show Kuts
forall a.
(BindId -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: BindId -> Kuts -> [Char] -> [Char]
showsPrec :: BindId -> Kuts -> [Char] -> [Char]
$cshow :: Kuts -> [Char]
show :: Kuts -> [Char]
$cshowList :: [Kuts] -> [Char] -> [Char]
showList :: [Kuts] -> [Char] -> [Char]
Show, (forall x. Kuts -> Rep Kuts x)
-> (forall x. Rep Kuts x -> Kuts) -> Generic Kuts
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
$cfrom :: forall x. Kuts -> Rep Kuts x
from :: forall x. Kuts -> Rep Kuts x
$cto :: forall x. Rep Kuts x -> Kuts
to :: forall x. Rep Kuts x -> Kuts
Generic)

instance Fixpoint Kuts where
  toFix :: Kuts -> Doc
toFix (KS HashSet KVar
s) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Doc
"cut " Doc -> Doc -> Doc
<->) (Doc -> Doc) -> (KVar -> Doc) -> KVar -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KVar -> Doc
forall a. Fixpoint a => a -> Doc
toFix (KVar -> Doc) -> [KVar] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [KVar] -> [KVar]
forall a. Ord a => [a] -> [a]
L.sort (HashSet KVar -> [KVar]
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) = KVar -> HashSet KVar -> Bool
forall 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 (HashSet KVar -> Kuts) -> HashSet KVar -> Kuts
forall a b. (a -> b) -> a -> b
$ HashSet KVar -> HashSet KVar -> HashSet KVar
forall a. Eq 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 HashSet KVar
forall a. HashSet a
S.empty
  mappend :: Kuts -> Kuts -> Kuts
mappend = Kuts -> Kuts -> Kuts
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]
   -> 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]
-> 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
  = FI { cm :: HashMap Integer (SubC a)
cm       = [(Integer, SubC a)] -> HashMap Integer (SubC a)
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList ([(Integer, SubC a)] -> HashMap Integer (SubC a))
-> [(Integer, SubC a)] -> HashMap Integer (SubC a)
forall a b. (a -> b) -> a -> b
$ [SubC a] -> [(Integer, SubC a)]
forall a. [SubC a] -> [(Integer, SubC a)]
addIds [SubC a]
cs
       , ws :: HashMap KVar (WfC a)
ws       = (WfC a -> WfC a -> WfC a)
-> [(KVar, WfC a)] -> HashMap KVar (WfC a)
forall k v. Hashable k => (v -> v -> v) -> [(k, v)] -> HashMap k v
M.fromListWith WfC a -> WfC a -> WfC a
forall {a}. a
err [(KVar
k, WfC a
w) | WfC a
w <- [WfC a]
ws, let (Symbol
_, Sort
_, KVar
k) = WfC a -> (Symbol, Sort, KVar)
forall a. WfC a -> (Symbol, Sort, KVar)
wrft WfC a
w]
       , bs :: BindEnv a
bs       = BindEnv a
binds
       , 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
       , lrws :: LocalRewritesEnv
lrws     = LocalRewritesEnv
forall a. Monoid a => a
mempty
       , defns :: DefinedFuns
defns    = DefinedFuns
forall a. Monoid a => a
mempty
       }
  where
    --TODO handle duplicates gracefully instead (merge envs by intersect?)
    err :: a
err = [Char] -> a
forall a. (?callStack::CallStack) => [Char] -> a
errorstar [Char]
"multiple WfCs with same kvar"

------------------------------------------------------------------------
-- | 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
(HOInfo -> HOInfo -> Bool)
-> (HOInfo -> HOInfo -> Bool) -> Eq HOInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HOInfo -> HOInfo -> Bool
== :: HOInfo -> HOInfo -> Bool
$c/= :: HOInfo -> HOInfo -> Bool
/= :: HOInfo -> HOInfo -> Bool
Eq, BindId -> HOInfo -> [Char] -> [Char]
[HOInfo] -> [Char] -> [Char]
HOInfo -> [Char]
(BindId -> HOInfo -> [Char] -> [Char])
-> (HOInfo -> [Char])
-> ([HOInfo] -> [Char] -> [Char])
-> Show HOInfo
forall a.
(BindId -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: BindId -> HOInfo -> [Char] -> [Char]
showsPrec :: BindId -> HOInfo -> [Char] -> [Char]
$cshow :: HOInfo -> [Char]
show :: HOInfo -> [Char]
$cshowList :: [HOInfo] -> [Char] -> [Char]
showList :: [HOInfo] -> [Char] -> [Char]
Show, (forall x. HOInfo -> Rep HOInfo x)
-> (forall x. Rep HOInfo x -> HOInfo) -> Generic HOInfo
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
$cfrom :: forall x. HOInfo -> Rep HOInfo x
from :: forall x. HOInfo -> Rep HOInfo x
$cto :: forall x. Rep HOInfo x -> HOInfo
to :: forall x. Rep HOInfo x -> HOInfo
Generic)

cfgHoInfo :: C.Config -> HOInfo
cfgHoInfo :: Config -> HOInfo
cfgHoInfo Config
cfg = Bool -> Bool -> HOInfo
HOI (Config -> Bool
C.allowHO Config
cfg) (Config -> Bool
C.allowHOqs Config
cfg)

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

data GInfo c a = FI
  { forall (c :: * -> *) a. GInfo c a -> HashMap Integer (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)               -- ^ BindId  |-> (Symbol, SortedReft)
  , 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
  , forall (c :: * -> *) a. GInfo c a -> LocalRewritesEnv
lrws     :: LocalRewritesEnv           -- ^ Local rewrites
  , forall (c :: * -> *) a. GInfo c a -> DefinedFuns
defns    :: DefinedFuns                -- ^ `define_fun` definitions to be passed to SMT
  }
  deriving (GInfo c a -> GInfo c a -> Bool
(GInfo c a -> GInfo c a -> Bool)
-> (GInfo c a -> GInfo c a -> Bool) -> Eq (GInfo c a)
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
$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
/= :: GInfo c a -> GInfo c a -> Bool
Eq, BindId -> GInfo c a -> [Char] -> [Char]
[GInfo c a] -> [Char] -> [Char]
GInfo c a -> [Char]
(BindId -> GInfo c a -> [Char] -> [Char])
-> (GInfo c a -> [Char])
-> ([GInfo c a] -> [Char] -> [Char])
-> Show (GInfo c a)
forall a.
(BindId -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
BindId -> GInfo c a -> [Char] -> [Char]
forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
[GInfo c a] -> [Char] -> [Char]
forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
GInfo c a -> [Char]
$cshowsPrec :: forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
BindId -> GInfo c a -> [Char] -> [Char]
showsPrec :: BindId -> GInfo c a -> [Char] -> [Char]
$cshow :: forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
GInfo c a -> [Char]
show :: GInfo c a -> [Char]
$cshowList :: forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
[GInfo c a] -> [Char] -> [Char]
showList :: [GInfo c a] -> [Char] -> [Char]
Show, (forall a b. (a -> b) -> GInfo c a -> GInfo c b)
-> (forall a b. a -> GInfo c b -> GInfo c a) -> Functor (GInfo c)
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
$cfmap :: forall (c :: * -> *) a b.
Functor c =>
(a -> b) -> GInfo c a -> GInfo c b
fmap :: forall a b. (a -> b) -> GInfo c a -> GInfo c b
$c<$ :: forall (c :: * -> *) a b. Functor c => a -> GInfo c b -> GInfo c a
<$ :: forall a b. a -> GInfo c b -> GInfo c a
Functor, (forall x. GInfo c a -> Rep (GInfo c a) x)
-> (forall x. Rep (GInfo c a) x -> GInfo c a)
-> Generic (GInfo c a)
forall x. Rep (GInfo c a) x -> GInfo c a
forall x. GInfo c a -> Rep (GInfo c a) x
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
$cfrom :: forall (c :: * -> *) a x. GInfo c a -> Rep (GInfo c a) x
from :: forall x. GInfo c a -> Rep (GInfo c a) x
$cto :: forall (c :: * -> *) a x. Rep (GInfo c a) x -> GInfo c a
to :: forall x. Rep (GInfo c a) x -> GInfo c a
Generic)

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 Integer (c a)
cm       = GInfo c a -> HashMap Integer (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm GInfo c a
i1       HashMap Integer (c a)
-> HashMap Integer (c a) -> HashMap Integer (c a)
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> HashMap Integer (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm GInfo c a
i2
                , ws :: HashMap KVar (WfC a)
ws       = GInfo c a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws GInfo c a
i1       HashMap KVar (WfC a)
-> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws GInfo c a
i2
                , bs :: BindEnv a
bs       = GInfo c a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs GInfo c a
i1       BindEnv a -> BindEnv a -> BindEnv a
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs GInfo c a
i2
                , gLits :: SEnv Sort
gLits    = GInfo c a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
gLits GInfo c a
i1    SEnv Sort -> SEnv Sort -> SEnv Sort
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
gLits GInfo c a
i2
                , dLits :: SEnv Sort
dLits    = GInfo c a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
dLits GInfo c a
i1    SEnv Sort -> SEnv Sort -> SEnv Sort
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
dLits GInfo c a
i2
                , kuts :: Kuts
kuts     = GInfo c a -> Kuts
forall (c :: * -> *) a. GInfo c a -> Kuts
kuts GInfo c a
i1     Kuts -> Kuts -> Kuts
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> Kuts
forall (c :: * -> *) a. GInfo c a -> Kuts
kuts GInfo c a
i2
                , quals :: [Qualifier]
quals    = GInfo c a -> [Qualifier]
forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals GInfo c a
i1    [Qualifier] -> [Qualifier] -> [Qualifier]
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> [Qualifier]
forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals GInfo c a
i2
                , bindInfo :: HashMap BindId a
bindInfo = GInfo c a -> HashMap BindId a
forall (c :: * -> *) a. GInfo c a -> HashMap BindId a
bindInfo GInfo c a
i1 HashMap BindId a -> HashMap BindId a -> HashMap BindId a
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> HashMap BindId a
forall (c :: * -> *) a. GInfo c a -> HashMap BindId a
bindInfo GInfo c a
i2
                , ddecls :: [DataDecl]
ddecls   = GInfo c a -> [DataDecl]
forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls GInfo c a
i1   [DataDecl] -> [DataDecl] -> [DataDecl]
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> [DataDecl]
forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls GInfo c a
i2
                , hoInfo :: HOInfo
hoInfo   = GInfo c a -> HOInfo
forall (c :: * -> *) a. GInfo c a -> HOInfo
hoInfo GInfo c a
i1   HOInfo -> HOInfo -> HOInfo
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> HOInfo
forall (c :: * -> *) a. GInfo c a -> HOInfo
hoInfo GInfo c a
i2
                , asserts :: [Triggered Expr]
asserts  = GInfo c a -> [Triggered Expr]
forall (c :: * -> *) a. GInfo c a -> [Triggered Expr]
asserts GInfo c a
i1  [Triggered Expr] -> [Triggered Expr] -> [Triggered Expr]
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> [Triggered Expr]
forall (c :: * -> *) a. GInfo c a -> [Triggered Expr]
asserts GInfo c a
i2
                , ae :: AxiomEnv
ae       = GInfo c a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae GInfo c a
i1       AxiomEnv -> AxiomEnv -> AxiomEnv
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae GInfo c a
i2
                , lrws :: LocalRewritesEnv
lrws     = GInfo c a -> LocalRewritesEnv
forall (c :: * -> *) a. GInfo c a -> LocalRewritesEnv
lrws GInfo c a
i1     LocalRewritesEnv -> LocalRewritesEnv -> LocalRewritesEnv
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> LocalRewritesEnv
forall (c :: * -> *) a. GInfo c a -> LocalRewritesEnv
lrws GInfo c a
i2
                , defns :: DefinedFuns
defns    = GInfo c a -> DefinedFuns
forall (c :: * -> *) a. GInfo c a -> DefinedFuns
defns GInfo c a
i1    DefinedFuns -> DefinedFuns -> DefinedFuns
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> DefinedFuns
forall (c :: * -> *) a. GInfo c a -> DefinedFuns
defns GInfo c a
i2
                }


instance Monoid (GInfo c a) where
  mempty :: GInfo c a
mempty        = FI { cm :: HashMap Integer (c a)
cm       = HashMap Integer (c a)
forall k v. HashMap k v
M.empty
                     , ws :: HashMap KVar (WfC a)
ws       = HashMap KVar (WfC a)
forall a. Monoid a => a
mempty
                     , bs :: BindEnv a
bs       = BindEnv a
forall a. Monoid a => a
mempty
                     , gLits :: SEnv Sort
gLits    = SEnv Sort
forall a. Monoid a => a
mempty
                     , dLits :: SEnv Sort
dLits    = SEnv Sort
forall a. Monoid a => a
mempty
                     , kuts :: Kuts
kuts     = Kuts
forall a. Monoid a => a
mempty
                     , quals :: [Qualifier]
quals    = [Qualifier]
forall a. Monoid a => a
mempty
                     , bindInfo :: HashMap BindId a
bindInfo = HashMap BindId a
forall a. Monoid a => a
mempty
                     , ddecls :: [DataDecl]
ddecls   = [DataDecl]
forall a. Monoid a => a
mempty
                     , hoInfo :: HOInfo
hoInfo   = HOInfo
forall a. Monoid a => a
mempty
                     , asserts :: [Triggered Expr]
asserts  = [Triggered Expr]
forall a. Monoid a => a
mempty
                     , ae :: AxiomEnv
ae       = AxiomEnv
forall a. Monoid a => a
mempty
                     , lrws :: LocalRewritesEnv
lrws     = LocalRewritesEnv
forall a. Monoid a => a
mempty
                     , defns :: DefinedFuns
defns    = DefinedFuns
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", BindId -> Doc
forall a. PPrint a => a -> Doc
pprint (BindId -> Doc) -> BindId -> Doc
forall a b. (a -> b) -> a -> b
$ HashMap Integer (SimpC a) -> BindId
forall a. HashMap Integer a -> BindId
forall (t :: * -> *) a. Foldable t => t a -> BindId
length (HashMap Integer (SimpC a) -> BindId)
-> HashMap Integer (SimpC a) -> BindId
forall a b. (a -> b) -> a -> b
$ SInfo a -> HashMap Integer (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm SInfo a
z)
                      , ([Char] -> Doc
text [Char]
"# WF  Constraints", BindId -> Doc
forall a. PPrint a => a -> Doc
pprint (BindId -> Doc) -> BindId -> Doc
forall a b. (a -> b) -> a -> b
$ HashMap KVar (WfC a) -> BindId
forall a. HashMap KVar a -> BindId
forall (t :: * -> *) a. Foldable t => t a -> BindId
length (HashMap KVar (WfC a) -> BindId) -> HashMap KVar (WfC a) -> BindId
forall a b. (a -> b) -> a -> b
$ SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws SInfo a
z)
                      ]

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

writeFInfo :: (Fixpoint a, Fixpoint (c a)) => C.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 (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ Config -> GInfo c a -> Doc
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 = subcToSimpc bindm <$> cm fi' }
  where
    (BindM
bindm, FInfo a
fi') = ((BindM, FInfo a) -> Integer -> SubC a -> (BindM, FInfo a))
-> (BindM, FInfo a) -> HashMap Integer (SubC a) -> (BindM, FInfo a)
forall a k v. (a -> k -> v -> a) -> a -> HashMap k v -> a
M.foldlWithKey' (BindM, FInfo a) -> Integer -> SubC a -> (BindM, FInfo a)
forall a. (BindM, FInfo a) -> Integer -> SubC a -> (BindM, FInfo a)
outVV (BindM
forall k v. HashMap k v
M.empty, FInfo a
fi) (HashMap Integer (SubC a) -> (BindM, FInfo a))
-> HashMap Integer (SubC a) -> (BindM, FInfo a)
forall a b. (a -> b) -> a -> b
$ FInfo a -> HashMap Integer (SubC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (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       = SubC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
s
  , _crhs :: Expr
_crhs       = ReftV Symbol -> Expr
forall v. ReftV v -> ExprV v
reftPred (ReftV Symbol -> Expr) -> ReftV Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ SortedReft -> ReftV Symbol
sr_reft (SortedReft -> ReftV Symbol) -> SortedReft -> ReftV Symbol
forall a b. (a -> b) -> a -> b
$ SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs SubC a
s
  , _cid :: Maybe Integer
_cid        = SubC a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
sid SubC a
s
  , cbind :: BindId
cbind      = [Char] -> Integer -> BindM -> BindId
forall k v.
(?callStack::CallStack, Eq k, Hashable k) =>
[Char] -> k -> HashMap k v -> v
safeLookup [Char]
"subcToSimpc" (SubC a -> Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Integer
subcId SubC a
s) BindM
m
  , _ctag :: Tag
_ctag       = SubC a -> Tag
forall (c :: * -> *) a. TaggedC c a => c a -> Tag
stag SubC a
s
  , _cinfo :: a
_cinfo      = SubC a -> a
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) -> Integer -> SubC a -> (BindM, FInfo a)
outVV (BindM
m, FInfo a
fi) Integer
i SubC a
c = (BindM
m', FInfo a
fi')
  where
    fi' :: FInfo a
fi'           = FInfo a
fi { bs = be', cm = cm' }
    m' :: BindM
m'            = Integer -> BindId -> BindM -> BindM
forall k v. Hashable k => k -> v -> HashMap k v -> HashMap k v
M.insert Integer
i BindId
bId BindM
m
    (BindId
bId, BindEnv a
be')    = Symbol -> SortedReft -> a -> BindEnv a -> (BindId, BindEnv a)
forall a.
Symbol -> SortedReft -> a -> BindEnv a -> (BindId, BindEnv a)
insertBindEnv Symbol
x SortedReft
sr (SubC a -> a
forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SubC a
c) (FInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs FInfo a
fi)
    cm' :: HashMap Integer (SubC a)
cm'           = Integer
-> SubC a -> HashMap Integer (SubC a) -> HashMap Integer (SubC a)
forall k v. Hashable k => k -> v -> HashMap k v -> HashMap k v
M.insert Integer
i SubC a
c' (HashMap Integer (SubC a) -> HashMap Integer (SubC a))
-> HashMap Integer (SubC a) -> HashMap Integer (SubC a)
forall a b. (a -> b) -> a -> b
$ FInfo a -> HashMap Integer (SubC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm FInfo a
fi
    c' :: SubC a
c'            = SubC a
c { _senv = insertsIBindEnv [bId] $ senv c }
    sr :: SortedReft
sr            = SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
c
    x :: Symbol
x             = ReftV Symbol -> Symbol
forall v. ReftV v -> Symbol
reftBind (ReftV Symbol -> Symbol) -> ReftV Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ SortedReft -> ReftV Symbol
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 = envWithoutLhss
  , cm = simpcToSubc (bs fi) <$> cm fi
  }
  where
    envWithoutLhss :: BindEnv a
envWithoutLhss =
      (BindEnv a -> SimpC a -> BindEnv a)
-> BindEnv a -> HashMap Integer (SimpC a) -> BindEnv a
forall a v k. (a -> v -> a) -> a -> HashMap k v -> a
M.foldl' (\BindEnv a
m SimpC a
c -> BindId -> BindEnv a -> BindEnv a
forall a. BindId -> BindEnv a -> BindEnv a
deleteBindEnv (SimpC a -> BindId
forall a. SimpC a -> BindId
cbind SimpC a
c) BindEnv a
m) (SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi) (SInfo a -> HashMap Integer (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (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 (SimpC a -> BindId
forall a. SimpC a -> BindId
cbind SimpC a
s) (SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC a
s)
  , slhs :: SortedReft
slhs   = SortedReft
sr
  , srhs :: SortedReft
srhs   = Sort -> ReftV Symbol -> SortedReft
RR (SortedReft -> Sort
sr_sort SortedReft
sr) ((Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
b, SimpC a -> Expr
forall a. SimpC a -> Expr
_crhs SimpC a
s))
  , _sid :: Maybe Integer
_sid   = SimpC a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
sid SimpC a
s
  , _stag :: Tag
_stag  = SimpC a -> Tag
forall (c :: * -> *) a. TaggedC c a => c a -> Tag
stag SimpC a
s
  , _sinfo :: a
_sinfo = SimpC a -> a
forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SimpC a
s
  }
  where
    (Symbol
b, SortedReft
sr, a
_) = BindId -> BindEnv a -> (Symbol, SortedReft, a)
forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv (SimpC a -> BindId
forall a. SimpC a -> BindId
cbind SimpC a
s) BindEnv a
env

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

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

saveTextQuery :: Fixpoint a => C.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]
C.queryFile Ext
Files.Fq Config
cfg
  [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Saving Text Query: "   [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
fq [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
  [Char] -> IO ()
ensurePath [Char]
fq
  [Char] -> Text -> IO ()
T.writeFile [Char]
fq (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Text
T.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
render (Config -> FInfo a -> Doc
forall a (c :: * -> *).
(Fixpoint a, Fixpoint (c a)) =>
Config -> GInfo c a -> Doc
toFixpoint Config
cfg FInfo a
fi)

-- | Used for debugging to inspect intermediate 'SInfo' files.
--
-- Takes a suffix to put in the name of the written file, whose name
-- is still derived from the input file name in `cfg`.
--
-- Usage example:
--
-- > when (save cfg) $
-- >   saveSInfo cfg ".sinfo" si
--
-- This will write a file like `.liquid/Test.hs.sinfo.fq` when the
-- `--save` flag is used.
--
saveSInfo :: Fixpoint a => C.Config -> String -> SInfo a -> IO ()
saveSInfo :: forall a. Fixpoint a => Config -> [Char] -> SInfo a -> IO ()
saveSInfo Config
cfg [Char]
sfx SInfo a
si = do
  let fq :: [Char]
fq = [Char] -> [Char]
Files.tempFileName (Config -> [Char]
C.srcFile Config
cfg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
sfx [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
".fq")
  [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Saving Text Query: "   [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
fq [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
  [Char] -> IO ()
ensurePath [Char]
fq
  [Char] -> Text -> IO ()
T.writeFile [Char]
fq (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Text
T.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
render (Config -> SInfo a -> Doc
forall a (c :: * -> *).
(Fixpoint a, Fixpoint (c a)) =>
Config -> GInfo c a -> Doc
toFixpoint Config
cfg SInfo a
si)

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

newtype LocalRewrites = LocalRewrites (M.HashMap Symbol Expr)
  deriving (LocalRewrites -> LocalRewrites -> Bool
(LocalRewrites -> LocalRewrites -> Bool)
-> (LocalRewrites -> LocalRewrites -> Bool) -> Eq LocalRewrites
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LocalRewrites -> LocalRewrites -> Bool
== :: LocalRewrites -> LocalRewrites -> Bool
$c/= :: LocalRewrites -> LocalRewrites -> Bool
/= :: LocalRewrites -> LocalRewrites -> Bool
Eq, BindId -> LocalRewrites -> [Char] -> [Char]
[LocalRewrites] -> [Char] -> [Char]
LocalRewrites -> [Char]
(BindId -> LocalRewrites -> [Char] -> [Char])
-> (LocalRewrites -> [Char])
-> ([LocalRewrites] -> [Char] -> [Char])
-> Show LocalRewrites
forall a.
(BindId -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: BindId -> LocalRewrites -> [Char] -> [Char]
showsPrec :: BindId -> LocalRewrites -> [Char] -> [Char]
$cshow :: LocalRewrites -> [Char]
show :: LocalRewrites -> [Char]
$cshowList :: [LocalRewrites] -> [Char] -> [Char]
showList :: [LocalRewrites] -> [Char] -> [Char]
Show, (forall x. LocalRewrites -> Rep LocalRewrites x)
-> (forall x. Rep LocalRewrites x -> LocalRewrites)
-> Generic LocalRewrites
forall x. Rep LocalRewrites x -> LocalRewrites
forall x. LocalRewrites -> Rep LocalRewrites x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LocalRewrites -> Rep LocalRewrites x
from :: forall x. LocalRewrites -> Rep LocalRewrites x
$cto :: forall x. Rep LocalRewrites x -> LocalRewrites
to :: forall x. Rep LocalRewrites x -> LocalRewrites
Generic, NonEmpty LocalRewrites -> LocalRewrites
LocalRewrites -> LocalRewrites -> LocalRewrites
(LocalRewrites -> LocalRewrites -> LocalRewrites)
-> (NonEmpty LocalRewrites -> LocalRewrites)
-> (forall b. Integral b => b -> LocalRewrites -> LocalRewrites)
-> Semigroup LocalRewrites
forall b. Integral b => b -> LocalRewrites -> LocalRewrites
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: LocalRewrites -> LocalRewrites -> LocalRewrites
<> :: LocalRewrites -> LocalRewrites -> LocalRewrites
$csconcat :: NonEmpty LocalRewrites -> LocalRewrites
sconcat :: NonEmpty LocalRewrites -> LocalRewrites
$cstimes :: forall b. Integral b => b -> LocalRewrites -> LocalRewrites
stimes :: forall b. Integral b => b -> LocalRewrites -> LocalRewrites
Semigroup, Semigroup LocalRewrites
LocalRewrites
Semigroup LocalRewrites =>
LocalRewrites
-> (LocalRewrites -> LocalRewrites -> LocalRewrites)
-> ([LocalRewrites] -> LocalRewrites)
-> Monoid LocalRewrites
[LocalRewrites] -> LocalRewrites
LocalRewrites -> LocalRewrites -> LocalRewrites
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: LocalRewrites
mempty :: LocalRewrites
$cmappend :: LocalRewrites -> LocalRewrites -> LocalRewrites
mappend :: LocalRewrites -> LocalRewrites -> LocalRewrites
$cmconcat :: [LocalRewrites] -> LocalRewrites
mconcat :: [LocalRewrites] -> LocalRewrites
Monoid, LocalRewrites -> ()
(LocalRewrites -> ()) -> NFData LocalRewrites
forall a. (a -> ()) -> NFData a
$crnf :: LocalRewrites -> ()
rnf :: LocalRewrites -> ()
NFData, Peek LocalRewrites
Size LocalRewrites
Size LocalRewrites
-> (LocalRewrites -> Poke ())
-> Peek LocalRewrites
-> Store LocalRewrites
LocalRewrites -> Poke ()
forall a. Size a -> (a -> Poke ()) -> Peek a -> Store a
$csize :: Size LocalRewrites
size :: Size LocalRewrites
$cpoke :: LocalRewrites -> Poke ()
poke :: LocalRewrites -> Poke ()
$cpeek :: Peek LocalRewrites
peek :: Peek LocalRewrites
S.Store)

newtype LocalRewritesEnv = LocalRewritesMap (M.HashMap BindId LocalRewrites)
  deriving (LocalRewritesEnv -> LocalRewritesEnv -> Bool
(LocalRewritesEnv -> LocalRewritesEnv -> Bool)
-> (LocalRewritesEnv -> LocalRewritesEnv -> Bool)
-> Eq LocalRewritesEnv
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LocalRewritesEnv -> LocalRewritesEnv -> Bool
== :: LocalRewritesEnv -> LocalRewritesEnv -> Bool
$c/= :: LocalRewritesEnv -> LocalRewritesEnv -> Bool
/= :: LocalRewritesEnv -> LocalRewritesEnv -> Bool
Eq, BindId -> LocalRewritesEnv -> [Char] -> [Char]
[LocalRewritesEnv] -> [Char] -> [Char]
LocalRewritesEnv -> [Char]
(BindId -> LocalRewritesEnv -> [Char] -> [Char])
-> (LocalRewritesEnv -> [Char])
-> ([LocalRewritesEnv] -> [Char] -> [Char])
-> Show LocalRewritesEnv
forall a.
(BindId -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: BindId -> LocalRewritesEnv -> [Char] -> [Char]
showsPrec :: BindId -> LocalRewritesEnv -> [Char] -> [Char]
$cshow :: LocalRewritesEnv -> [Char]
show :: LocalRewritesEnv -> [Char]
$cshowList :: [LocalRewritesEnv] -> [Char] -> [Char]
showList :: [LocalRewritesEnv] -> [Char] -> [Char]
Show, (forall x. LocalRewritesEnv -> Rep LocalRewritesEnv x)
-> (forall x. Rep LocalRewritesEnv x -> LocalRewritesEnv)
-> Generic LocalRewritesEnv
forall x. Rep LocalRewritesEnv x -> LocalRewritesEnv
forall x. LocalRewritesEnv -> Rep LocalRewritesEnv x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LocalRewritesEnv -> Rep LocalRewritesEnv x
from :: forall x. LocalRewritesEnv -> Rep LocalRewritesEnv x
$cto :: forall x. Rep LocalRewritesEnv x -> LocalRewritesEnv
to :: forall x. Rep LocalRewritesEnv x -> LocalRewritesEnv
Generic, NonEmpty LocalRewritesEnv -> LocalRewritesEnv
LocalRewritesEnv -> LocalRewritesEnv -> LocalRewritesEnv
(LocalRewritesEnv -> LocalRewritesEnv -> LocalRewritesEnv)
-> (NonEmpty LocalRewritesEnv -> LocalRewritesEnv)
-> (forall b.
    Integral b =>
    b -> LocalRewritesEnv -> LocalRewritesEnv)
-> Semigroup LocalRewritesEnv
forall b. Integral b => b -> LocalRewritesEnv -> LocalRewritesEnv
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: LocalRewritesEnv -> LocalRewritesEnv -> LocalRewritesEnv
<> :: LocalRewritesEnv -> LocalRewritesEnv -> LocalRewritesEnv
$csconcat :: NonEmpty LocalRewritesEnv -> LocalRewritesEnv
sconcat :: NonEmpty LocalRewritesEnv -> LocalRewritesEnv
$cstimes :: forall b. Integral b => b -> LocalRewritesEnv -> LocalRewritesEnv
stimes :: forall b. Integral b => b -> LocalRewritesEnv -> LocalRewritesEnv
Semigroup, Semigroup LocalRewritesEnv
LocalRewritesEnv
Semigroup LocalRewritesEnv =>
LocalRewritesEnv
-> (LocalRewritesEnv -> LocalRewritesEnv -> LocalRewritesEnv)
-> ([LocalRewritesEnv] -> LocalRewritesEnv)
-> Monoid LocalRewritesEnv
[LocalRewritesEnv] -> LocalRewritesEnv
LocalRewritesEnv -> LocalRewritesEnv -> LocalRewritesEnv
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: LocalRewritesEnv
mempty :: LocalRewritesEnv
$cmappend :: LocalRewritesEnv -> LocalRewritesEnv -> LocalRewritesEnv
mappend :: LocalRewritesEnv -> LocalRewritesEnv -> LocalRewritesEnv
$cmconcat :: [LocalRewritesEnv] -> LocalRewritesEnv
mconcat :: [LocalRewritesEnv] -> LocalRewritesEnv
Monoid, LocalRewritesEnv -> ()
(LocalRewritesEnv -> ()) -> NFData LocalRewritesEnv
forall a. (a -> ()) -> NFData a
$crnf :: LocalRewritesEnv -> ()
rnf :: LocalRewritesEnv -> ()
NFData, Peek LocalRewritesEnv
Size LocalRewritesEnv
Size LocalRewritesEnv
-> (LocalRewritesEnv -> Poke ())
-> Peek LocalRewritesEnv
-> Store LocalRewritesEnv
LocalRewritesEnv -> Poke ()
forall a. Size a -> (a -> Poke ()) -> Peek a -> Store a
$csize :: Size LocalRewritesEnv
size :: Size LocalRewritesEnv
$cpoke :: LocalRewritesEnv -> Poke ()
poke :: LocalRewritesEnv -> Poke ()
$cpeek :: Peek LocalRewritesEnv
peek :: Peek LocalRewritesEnv
S.Store)

lookupRewrite :: Symbol -> LocalRewrites -> Maybe Expr
lookupRewrite :: Symbol -> LocalRewrites -> Maybe Expr
lookupRewrite Symbol
x (LocalRewrites HashMap Symbol Expr
m) = Symbol -> HashMap Symbol Expr -> Maybe Expr
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Symbol
x HashMap Symbol Expr
m

lookupLocalRewrites :: BindId -> LocalRewritesEnv -> Maybe LocalRewrites
lookupLocalRewrites :: BindId -> LocalRewritesEnv -> Maybe LocalRewrites
lookupLocalRewrites BindId
i (LocalRewritesMap HashMap BindId LocalRewrites
m) = BindId -> HashMap BindId LocalRewrites -> Maybe LocalRewrites
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup BindId
i HashMap BindId LocalRewrites
m

insertRewrites :: BindId -> LocalRewrites -> LocalRewritesEnv -> LocalRewritesEnv
insertRewrites :: BindId -> LocalRewrites -> LocalRewritesEnv -> LocalRewritesEnv
insertRewrites BindId
i LocalRewrites
rws (LocalRewritesMap HashMap BindId LocalRewrites
m) = HashMap BindId LocalRewrites -> LocalRewritesEnv
LocalRewritesMap (HashMap BindId LocalRewrites -> LocalRewritesEnv)
-> HashMap BindId LocalRewrites -> LocalRewritesEnv
forall a b. (a -> b) -> a -> b
$ (LocalRewrites -> LocalRewrites -> LocalRewrites)
-> BindId
-> LocalRewrites
-> HashMap BindId LocalRewrites
-> HashMap BindId LocalRewrites
forall k v.
Hashable k =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
M.insertWith LocalRewrites -> LocalRewrites -> LocalRewrites
forall a. Semigroup a => a -> a -> a
(<>) BindId
i LocalRewrites
rws HashMap BindId LocalRewrites
m


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

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

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

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

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


newtype DefinedFuns = MkDefinedFuns [Equation]
  deriving (Typeable DefinedFuns
Typeable DefinedFuns =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> DefinedFuns -> c DefinedFuns)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DefinedFuns)
-> (DefinedFuns -> Constr)
-> (DefinedFuns -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DefinedFuns))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DefinedFuns))
-> ((forall b. Data b => b -> b) -> DefinedFuns -> DefinedFuns)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DefinedFuns -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DefinedFuns -> r)
-> (forall u. (forall d. Data d => d -> u) -> DefinedFuns -> [u])
-> (forall u.
    BindId -> (forall d. Data d => d -> u) -> DefinedFuns -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> DefinedFuns -> m DefinedFuns)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DefinedFuns -> m DefinedFuns)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DefinedFuns -> m DefinedFuns)
-> Data DefinedFuns
DefinedFuns -> Constr
DefinedFuns -> DataType
(forall b. Data b => b -> b) -> DefinedFuns -> DefinedFuns
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) -> DefinedFuns -> u
forall u. (forall d. Data d => d -> u) -> DefinedFuns -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DefinedFuns -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DefinedFuns -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DefinedFuns -> m DefinedFuns
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DefinedFuns -> m DefinedFuns
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DefinedFuns
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DefinedFuns -> c DefinedFuns
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DefinedFuns)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DefinedFuns)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DefinedFuns -> c DefinedFuns
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DefinedFuns -> c DefinedFuns
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DefinedFuns
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DefinedFuns
$ctoConstr :: DefinedFuns -> Constr
toConstr :: DefinedFuns -> Constr
$cdataTypeOf :: DefinedFuns -> DataType
dataTypeOf :: DefinedFuns -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DefinedFuns)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DefinedFuns)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DefinedFuns)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DefinedFuns)
$cgmapT :: (forall b. Data b => b -> b) -> DefinedFuns -> DefinedFuns
gmapT :: (forall b. Data b => b -> b) -> DefinedFuns -> DefinedFuns
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DefinedFuns -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DefinedFuns -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DefinedFuns -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DefinedFuns -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DefinedFuns -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> DefinedFuns -> [u]
$cgmapQi :: forall u.
BindId -> (forall d. Data d => d -> u) -> DefinedFuns -> u
gmapQi :: forall u.
BindId -> (forall d. Data d => d -> u) -> DefinedFuns -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DefinedFuns -> m DefinedFuns
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DefinedFuns -> m DefinedFuns
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DefinedFuns -> m DefinedFuns
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DefinedFuns -> m DefinedFuns
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DefinedFuns -> m DefinedFuns
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DefinedFuns -> m DefinedFuns
Data, DefinedFuns -> DefinedFuns -> Bool
(DefinedFuns -> DefinedFuns -> Bool)
-> (DefinedFuns -> DefinedFuns -> Bool) -> Eq DefinedFuns
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DefinedFuns -> DefinedFuns -> Bool
== :: DefinedFuns -> DefinedFuns -> Bool
$c/= :: DefinedFuns -> DefinedFuns -> Bool
/= :: DefinedFuns -> DefinedFuns -> Bool
Eq, Eq DefinedFuns
Eq DefinedFuns =>
(DefinedFuns -> DefinedFuns -> Ordering)
-> (DefinedFuns -> DefinedFuns -> Bool)
-> (DefinedFuns -> DefinedFuns -> Bool)
-> (DefinedFuns -> DefinedFuns -> Bool)
-> (DefinedFuns -> DefinedFuns -> Bool)
-> (DefinedFuns -> DefinedFuns -> DefinedFuns)
-> (DefinedFuns -> DefinedFuns -> DefinedFuns)
-> Ord DefinedFuns
DefinedFuns -> DefinedFuns -> Bool
DefinedFuns -> DefinedFuns -> Ordering
DefinedFuns -> DefinedFuns -> DefinedFuns
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
$ccompare :: DefinedFuns -> DefinedFuns -> Ordering
compare :: DefinedFuns -> DefinedFuns -> Ordering
$c< :: DefinedFuns -> DefinedFuns -> Bool
< :: DefinedFuns -> DefinedFuns -> Bool
$c<= :: DefinedFuns -> DefinedFuns -> Bool
<= :: DefinedFuns -> DefinedFuns -> Bool
$c> :: DefinedFuns -> DefinedFuns -> Bool
> :: DefinedFuns -> DefinedFuns -> Bool
$c>= :: DefinedFuns -> DefinedFuns -> Bool
>= :: DefinedFuns -> DefinedFuns -> Bool
$cmax :: DefinedFuns -> DefinedFuns -> DefinedFuns
max :: DefinedFuns -> DefinedFuns -> DefinedFuns
$cmin :: DefinedFuns -> DefinedFuns -> DefinedFuns
min :: DefinedFuns -> DefinedFuns -> DefinedFuns
Ord, BindId -> DefinedFuns -> [Char] -> [Char]
[DefinedFuns] -> [Char] -> [Char]
DefinedFuns -> [Char]
(BindId -> DefinedFuns -> [Char] -> [Char])
-> (DefinedFuns -> [Char])
-> ([DefinedFuns] -> [Char] -> [Char])
-> Show DefinedFuns
forall a.
(BindId -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: BindId -> DefinedFuns -> [Char] -> [Char]
showsPrec :: BindId -> DefinedFuns -> [Char] -> [Char]
$cshow :: DefinedFuns -> [Char]
show :: DefinedFuns -> [Char]
$cshowList :: [DefinedFuns] -> [Char] -> [Char]
showList :: [DefinedFuns] -> [Char] -> [Char]
Show, (forall x. DefinedFuns -> Rep DefinedFuns x)
-> (forall x. Rep DefinedFuns x -> DefinedFuns)
-> Generic DefinedFuns
forall x. Rep DefinedFuns x -> DefinedFuns
forall x. DefinedFuns -> Rep DefinedFuns x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DefinedFuns -> Rep DefinedFuns x
from :: forall x. DefinedFuns -> Rep DefinedFuns x
$cto :: forall x. Rep DefinedFuns x -> DefinedFuns
to :: forall x. Rep DefinedFuns x -> DefinedFuns
Generic)

instance Semigroup DefinedFuns where
  MkDefinedFuns [Equation]
eq1 <> :: DefinedFuns -> DefinedFuns -> DefinedFuns
<> MkDefinedFuns [Equation]
eq2 = [Equation] -> DefinedFuns
MkDefinedFuns ([Equation]
eq1 [Equation] -> [Equation] -> [Equation]
forall a. Semigroup a => a -> a -> a
<> [Equation]
eq2)

instance Monoid DefinedFuns where
  mempty :: DefinedFuns
mempty = [Equation] -> DefinedFuns
MkDefinedFuns []

instance PPrint DefinedFuns where
  pprintTidy :: Tidy -> DefinedFuns -> Doc
pprintTidy Tidy
k (MkDefinedFuns [Equation]
eqs) = Tidy -> [Equation] -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k [Equation]
eqs

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

eqnToHornSMT :: Doc -> Equation -> Doc
eqnToHornSMT :: Doc -> Equation -> Doc
eqnToHornSMT Doc
keyword (Equ Symbol
f [(Symbol, Sort)]
xs Expr
e Sort
s Bool
_) = Doc -> Doc
parens (Doc
keyword Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
f Doc -> Doc -> Doc
<+> [(Symbol, Sort)] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [(Symbol, Sort)]
xs Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Sort
s Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Expr
e)


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
forall v.
Symbol
-> [(Symbol, Sort)] -> ExprV v -> Sort -> Bool -> EquationV v
Equ Symbol
f [(Symbol, Sort)]
xts Expr
e Sort
out (Symbol
f Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms Expr
e)

instance Subable Equation where
  syms :: Equation -> [Symbol]
syms   Equation
a = Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms (Equation -> Expr
forall v. EquationV v -> ExprV v
eqBody Equation
a) -- ++ F.syms (axiomEq a)
  subst :: (?callStack::CallStack) => SubstV Symbol -> Equation -> Equation
subst SubstV Symbol
su = (Expr -> Expr) -> Equation -> Equation
mapEqBody (SubstV Symbol -> Expr -> Expr
forall a.
(Subable a, ?callStack::CallStack) =>
SubstV Symbol -> a -> a
subst SubstV Symbol
su)
  substf :: (Symbol -> Expr) -> Equation -> Equation
substf Symbol -> Expr
f = (Expr -> Expr) -> Equation -> Equation
mapEqBody ((Symbol -> Expr) -> Expr -> Expr
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 ((Symbol -> Symbol) -> Expr -> Expr
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 = f (eqBody a) }

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

ppArgs :: (PPrint a) => [a] -> Doc
ppArgs :: forall a. PPrint a => [a] -> Doc
ppArgs = Doc -> Doc
parens (Doc -> Doc) -> ([a] -> Doc) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> Doc
intersperse Doc
", " ([Doc] -> Doc) -> ([a] -> [Doc]) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Doc
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
(AutoRewrite -> AutoRewrite -> Bool)
-> (AutoRewrite -> AutoRewrite -> Bool) -> Eq AutoRewrite
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AutoRewrite -> AutoRewrite -> Bool
== :: AutoRewrite -> AutoRewrite -> Bool
$c/= :: AutoRewrite -> AutoRewrite -> Bool
/= :: AutoRewrite -> AutoRewrite -> Bool
Eq, Eq AutoRewrite
Eq AutoRewrite =>
(AutoRewrite -> AutoRewrite -> Ordering)
-> (AutoRewrite -> AutoRewrite -> Bool)
-> (AutoRewrite -> AutoRewrite -> Bool)
-> (AutoRewrite -> AutoRewrite -> Bool)
-> (AutoRewrite -> AutoRewrite -> Bool)
-> (AutoRewrite -> AutoRewrite -> AutoRewrite)
-> (AutoRewrite -> AutoRewrite -> AutoRewrite)
-> Ord 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
$ccompare :: AutoRewrite -> AutoRewrite -> Ordering
compare :: AutoRewrite -> AutoRewrite -> Ordering
$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
>= :: AutoRewrite -> AutoRewrite -> Bool
$cmax :: AutoRewrite -> AutoRewrite -> AutoRewrite
max :: AutoRewrite -> AutoRewrite -> AutoRewrite
$cmin :: AutoRewrite -> AutoRewrite -> AutoRewrite
min :: AutoRewrite -> AutoRewrite -> AutoRewrite
Ord, BindId -> AutoRewrite -> [Char] -> [Char]
[AutoRewrite] -> [Char] -> [Char]
AutoRewrite -> [Char]
(BindId -> AutoRewrite -> [Char] -> [Char])
-> (AutoRewrite -> [Char])
-> ([AutoRewrite] -> [Char] -> [Char])
-> Show AutoRewrite
forall a.
(BindId -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: BindId -> AutoRewrite -> [Char] -> [Char]
showsPrec :: BindId -> AutoRewrite -> [Char] -> [Char]
$cshow :: AutoRewrite -> [Char]
show :: AutoRewrite -> [Char]
$cshowList :: [AutoRewrite] -> [Char] -> [Char]
showList :: [AutoRewrite] -> [Char] -> [Char]
Show, (forall x. AutoRewrite -> Rep AutoRewrite x)
-> (forall x. Rep AutoRewrite x -> AutoRewrite)
-> Generic AutoRewrite
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
$cfrom :: forall x. AutoRewrite -> Rep AutoRewrite x
from :: forall x. AutoRewrite -> Rep AutoRewrite x
$cto :: forall x. Rep AutoRewrite x -> AutoRewrite
to :: forall x. Rep AutoRewrite x -> AutoRewrite
Generic)

instance Hashable AutoRewrite


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

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

      rwsMapping :: [Doc]
rwsMapping = do
        (Integer
cid, [AutoRewrite]
rws) <- HashMap Integer [AutoRewrite] -> [(Integer, [AutoRewrite])]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Integer [AutoRewrite]
autoRW
        AutoRewrite
rw         <-  [AutoRewrite]
rws
        Doc -> [Doc]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> [Doc]) -> Doc -> [Doc]
forall a b. (a -> b) -> a -> b
$ Doc
"rewrite" Doc -> Doc -> Doc
<+> Doc -> Doc
brackets ([Char] -> Doc
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
cid [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ BindId -> [Char]
forall a. Show a => a -> [Char]
show (AutoRewrite -> BindId
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
Typeable Rewrite =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Rewrite -> c Rewrite)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Rewrite)
-> (Rewrite -> Constr)
-> (Rewrite -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> Rewrite -> Rewrite)
-> (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 u. (forall d. Data d => d -> u) -> Rewrite -> [u])
-> (forall u.
    BindId -> (forall d. Data d => d -> u) -> Rewrite -> u)
-> (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 (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Rewrite -> m Rewrite)
-> Data Rewrite
Rewrite -> Constr
Rewrite -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rewrite -> c Rewrite
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rewrite -> c Rewrite
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Rewrite
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Rewrite
$ctoConstr :: Rewrite -> Constr
toConstr :: Rewrite -> Constr
$cdataTypeOf :: Rewrite -> DataType
dataTypeOf :: Rewrite -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Rewrite)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Rewrite)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Rewrite)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Rewrite)
$cgmapT :: (forall b. Data b => b -> b) -> Rewrite -> Rewrite
gmapT :: (forall b. Data b => b -> b) -> Rewrite -> Rewrite
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Rewrite -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Rewrite -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Rewrite -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Rewrite -> [u]
$cgmapQi :: forall u. BindId -> (forall d. Data d => d -> u) -> Rewrite -> u
gmapQi :: forall u. BindId -> (forall d. Data d => d -> u) -> Rewrite -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
Data, Rewrite -> Rewrite -> Bool
(Rewrite -> Rewrite -> Bool)
-> (Rewrite -> Rewrite -> Bool) -> Eq Rewrite
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Rewrite -> Rewrite -> Bool
== :: Rewrite -> Rewrite -> Bool
$c/= :: Rewrite -> Rewrite -> Bool
/= :: Rewrite -> Rewrite -> Bool
Eq, Eq Rewrite
Eq Rewrite =>
(Rewrite -> Rewrite -> Ordering)
-> (Rewrite -> Rewrite -> Bool)
-> (Rewrite -> Rewrite -> Bool)
-> (Rewrite -> Rewrite -> Bool)
-> (Rewrite -> Rewrite -> Bool)
-> (Rewrite -> Rewrite -> Rewrite)
-> (Rewrite -> Rewrite -> Rewrite)
-> Ord 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
$ccompare :: Rewrite -> Rewrite -> Ordering
compare :: Rewrite -> Rewrite -> Ordering
$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
>= :: Rewrite -> Rewrite -> Bool
$cmax :: Rewrite -> Rewrite -> Rewrite
max :: Rewrite -> Rewrite -> Rewrite
$cmin :: Rewrite -> Rewrite -> Rewrite
min :: Rewrite -> Rewrite -> Rewrite
Ord, BindId -> Rewrite -> [Char] -> [Char]
[Rewrite] -> [Char] -> [Char]
Rewrite -> [Char]
(BindId -> Rewrite -> [Char] -> [Char])
-> (Rewrite -> [Char])
-> ([Rewrite] -> [Char] -> [Char])
-> Show Rewrite
forall a.
(BindId -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: BindId -> Rewrite -> [Char] -> [Char]
showsPrec :: BindId -> Rewrite -> [Char] -> [Char]
$cshow :: Rewrite -> [Char]
show :: Rewrite -> [Char]
$cshowList :: [Rewrite] -> [Char] -> [Char]
showList :: [Rewrite] -> [Char] -> [Char]
Show, (forall x. Rewrite -> Rep Rewrite x)
-> (forall x. Rep Rewrite x -> Rewrite) -> Generic Rewrite
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
$cfrom :: forall x. Rewrite -> Rep Rewrite x
from :: forall x. Rewrite -> Rep Rewrite x
$cto :: forall x. Rep Rewrite x -> Rewrite
to :: forall x. Rep Rewrite x -> Rewrite
Generic)

instance ToHornSMT Rewrite where
  toHornSMT :: Rewrite -> Doc
toHornSMT (SMeasure Symbol
f Symbol
d [Symbol]
xs Expr
e) =  Doc -> Doc
parens (Doc
"match" Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Symbol
f Doc -> Doc -> Doc
<+> [Symbol] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (Symbol
dSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
xs) Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Expr
e)



instance Fixpoint AxiomEnv where
  toFix :: AxiomEnv -> Doc
toFix AxiomEnv
axe = [Doc] -> Doc
vcat ((Equation -> Doc
forall a. Fixpoint a => a -> Doc
toFix (Equation -> Doc) -> [Equation] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Equation] -> [Equation]
forall a. Ord a => [a] -> [a]
L.sort (AxiomEnv -> [Equation]
aenvEqs AxiomEnv
axe)) [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ (Rewrite -> Doc
forall a. Fixpoint a => a -> Doc
toFix (Rewrite -> Doc) -> [Rewrite] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Rewrite] -> [Rewrite]
forall a. Ord a => [a] -> [a]
L.sort (AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
axe)))
              Doc -> Doc -> Doc
$+$ [Doc] -> Doc
forall {a}. Fixpoint a => [a] -> Doc
renderExpand ((Integer, Bool) -> Doc
forall {a} {a}. (Show a, Show a) => (a, a) -> Doc
pairdoc ((Integer, Bool) -> Doc) -> [(Integer, Bool)] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Integer, Bool)] -> [(Integer, Bool)]
forall a. Ord a => [a] -> [a]
L.sort (HashMap Integer Bool -> [(Integer, Bool)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Integer Bool -> [(Integer, Bool)])
-> HashMap Integer Bool -> [(Integer, Bool)]
forall a b. (a -> b) -> a -> b
$ AxiomEnv -> HashMap Integer Bool
aenvExpand AxiomEnv
axe))
              Doc -> Doc -> Doc
$+$ HashMap Integer [AutoRewrite] -> Doc
forall a. Fixpoint a => a -> Doc
toFix (AxiomEnv -> HashMap Integer [AutoRewrite]
aenvAutoRW AxiomEnv
axe)
    where
      pairdoc :: (a, a) -> Doc
pairdoc (a
x,a
y) = [Char] -> Doc
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ a -> [Char]
forall a. Show a => a -> [Char]
show a
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
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
<+> [a] -> 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
<+> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
f Doc -> Doc -> Doc
<+> [(Symbol, Sort)] -> Doc
forall a. PPrint a => [a] -> Doc
ppArgs [(Symbol, Sort)]
xs Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Sort -> 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 (Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix Expr
e))

instance Fixpoint LocalRewritesEnv where
  toFix :: LocalRewritesEnv -> Doc
toFix (LocalRewritesMap HashMap BindId LocalRewrites
rws) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (BindId -> LocalRewrites -> Doc) -> (BindId, LocalRewrites) -> Doc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry BindId -> LocalRewrites -> Doc
forall {a}. Fixpoint a => a -> LocalRewrites -> Doc
toFixLocal ((BindId, LocalRewrites) -> Doc)
-> [(BindId, LocalRewrites)] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap BindId LocalRewrites -> [(BindId, LocalRewrites)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap BindId LocalRewrites
rws
    where
      toFixLocal :: a -> LocalRewrites -> Doc
toFixLocal a
bid (LocalRewrites HashMap Symbol Expr
rws) = [Char] -> Doc
text [Char]
"defineLocal" Doc -> Doc -> Doc
<+> a -> Doc
forall a. Fixpoint a => a -> Doc
toFix a
bid
        Doc -> Doc -> Doc
<+> Doc -> Doc
brackets ([Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
";" ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Symbol -> Expr -> Doc) -> (Symbol, Expr) -> Doc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> Expr -> Doc
forall {a} {a}. (Fixpoint a, Fixpoint a) => a -> a -> Doc
toFixRewrite ((Symbol, Expr) -> Doc) -> [(Symbol, Expr)] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap Symbol Expr -> [(Symbol, Expr)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Symbol Expr
rws)
      toFixRewrite :: a -> a -> Doc
toFixRewrite a
sym a
eq = a -> Doc
forall a. Fixpoint a => a -> Doc
toFix a
sym Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
":=" Doc -> Doc -> Doc
<+> a -> Doc
forall a. Fixpoint a => a -> Doc
toFix a
eq

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
<+> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
f
   Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
d Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep (Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix (Symbol -> Doc) -> [Symbol] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs)
   Doc -> Doc -> Doc
<+> Doc -> Doc
braces (Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix Expr
e)

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