{-# 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     #-}

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

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

   -- * Serializing
  , toFixpoint
  , writeFInfo
  , saveQuery

   -- * Constructing Queries
  , fi

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

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

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

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

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

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

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

  -- * 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 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
                    }
             | GWfC { wenv  :: !IBindEnv
                    , wrft  :: !(Symbol, Sort, KVar)
                    , winfo :: !a
                    , forall a. WfC a -> Expr
wexpr :: !Expr
                    , forall a. WfC a -> GradInfo
wloc  :: !GradInfo
                    }
              deriving (WfC a -> WfC a -> Bool
(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)

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

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

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

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

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

type SubcId = Integer

data SubC a = SubC
  { forall a. SubC a -> IBindEnv
_senv  :: !IBindEnv
  , forall a. SubC a -> SortedReft
slhs   :: !SortedReft
  , forall a. SubC a -> SortedReft
srhs   :: !SortedReft
  , forall a. SubC a -> Maybe 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)] -> SInfo a
strengthenHyp :: forall a. SInfo a -> [(Integer, Expr)] -> SInfo a
strengthenHyp SInfo a
si [(Integer, Expr)]
ies = SInfo a -> HashMap BindId Expr -> SInfo a
forall a. SInfo a -> HashMap BindId Expr -> SInfo 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. (Eq k, 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 -> SInfo a
strengthenBinds :: forall a. SInfo a -> HashMap BindId Expr -> SInfo a
strengthenBinds SInfo a
si HashMap BindId Expr
m = SInfo a
si { bs = mapBindEnv f (bs 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. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup BindId
i HashMap BindId Expr
m of
                         Maybe Expr
Nothing -> (Symbol
x, SortedReft
sr, a
l)
                         Just Expr
e  -> (Symbol
x, SortedReft -> Expr -> SortedReft
strengthenSortedReft SortedReft
sr Expr
e, a
l)

strengthenSortedReft :: SortedReft -> Expr -> SortedReft
strengthenSortedReft :: SortedReft -> Expr -> SortedReft
strengthenSortedReft (RR Sort
s (Reft (Symbol
v, Expr
r))) Expr
e = Sort -> ReftV Symbol -> SortedReft
RR Sort
s ((Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
v, [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
---------------------------------------------------------------------------

type GFixSolution = GFixSol Expr

type FixSolution  = M.HashMap KVar Expr

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

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


data Result a = Result
  { forall a. Result a -> FixResult a
resStatus    :: !(FixResult a)
  , forall a. Result a -> FixSolution
resSolution  :: !FixSolution
  , forall a. Result a -> FixSolution
resNonCutsSolution :: !FixSolution
  , forall a. Result a -> GFixSolution
gresSolution :: !GFixSolution
  }
  deriving ((forall 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)



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

instance Semigroup (Result a) where
  Result a
r1 <> :: Result a -> Result a -> Result a
<> Result a
r2  = FixResult a
-> FixSolution -> FixSolution -> GFixSolution -> Result a
forall a.
FixResult a
-> FixSolution -> FixSolution -> GFixSolution -> Result a
Result FixResult a
stat FixSolution
soln FixSolution
nonCutsSoln GFixSolution
gsoln
    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 :: FixSolution
nonCutsSoln = Result a -> FixSolution
forall a. Result a -> FixSolution
resNonCutsSolution Result a
r1 FixSolution -> FixSolution -> FixSolution
forall a. Semigroup a => a -> a -> a
<> Result a -> FixSolution
forall a. Result a -> FixSolution
resNonCutsSolution Result a
r2
      gsoln :: GFixSolution
gsoln = Result a -> GFixSolution
forall a. Result a -> GFixSolution
gresSolution Result a
r1 GFixSolution -> GFixSolution -> GFixSolution
forall a. Semigroup a => a -> a -> a
<> Result a -> GFixSolution
forall a. Result a -> GFixSolution
gresSolution Result a
r2

instance Monoid (Result a) where
  mempty :: Result a
mempty        = FixResult a
-> FixSolution -> FixSolution -> GFixSolution -> Result a
forall a.
FixResult a
-> FixSolution -> FixSolution -> GFixSolution -> Result a
Result FixResult a
forall a. Monoid a => a
mempty FixSolution
forall a. Monoid a => a
mempty FixSolution
forall a. Monoid a => a
mempty GFixSolution
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))
              Doc -> Doc -> Doc
$+$ if WfC a -> Bool
forall a. WfC a -> Bool
isGWfc WfC a
w then Doc -> Doc -> Doc
toFixMeta ([Char] -> Doc
text [Char]
"expr") (Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix (WfC a -> Expr
forall a. WfC a -> Expr
wexpr WfC a
w)) else Doc
forall a. Monoid a => a
mempty
          (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 PPrint GFixSolution where
  pprintTidy :: Tidy -> GFixSolution -> Doc
pprintTidy Tidy
k (GSol HashMap KVar (Expr, [Expr])
xs) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
"\n\n" (Tidy -> (KVar, (Expr, [Expr])) -> Doc
pprintTidyGradual Tidy
k ((KVar, (Expr, [Expr])) -> Doc)
-> [(KVar, (Expr, [Expr]))] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap KVar (Expr, [Expr]) -> [(KVar, (Expr, [Expr]))]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap KVar (Expr, [Expr])
xs)

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

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

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

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

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

instance NFData QualPattern
instance NFData QualParam
instance NFData v => NFData (QualifierV v)
instance NFData Kuts
instance NFData HOInfo
instance NFData GFixSolution
instance NFData GWInfo

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

instance Hashable 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 ]
                  [WfC a] -> [WfC a] -> [WfC a]
forall a. [a] -> [a] -> [a]
++ [IBindEnv -> (Symbol, Sort, KVar) -> a -> Expr -> GradInfo -> WfC a
forall a.
IBindEnv -> (Symbol, Sort, KVar) -> a -> Expr -> GradInfo -> WfC a
GWfC IBindEnv
be (Symbol
v, SortedReft -> Sort
sr_sort SortedReft
sr, KVar
k) a
x Expr
e GradInfo
i | (KVar
k, Expr
e, GradInfo
i) <- [(KVar, Expr, GradInfo)]
gs ]
                else [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 [SubstV Symbol] -> [SubstV Symbol] -> [SubstV Symbol]
forall a. [a] -> [a] -> [a]
++ [SubstV Symbol]
gsus)
    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
    ([(KVar, Expr, GradInfo)]
gs, [SubstV Symbol]
gsus)      = [((KVar, Expr, GradInfo), SubstV Symbol)]
-> ([(KVar, Expr, GradInfo)], [SubstV Symbol])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((KVar, Expr, GradInfo), SubstV Symbol)]
 -> ([(KVar, Expr, GradInfo)], [SubstV Symbol]))
-> [((KVar, Expr, GradInfo), SubstV Symbol)]
-> ([(KVar, Expr, GradInfo)], [SubstV Symbol])
forall a b. (a -> b) -> a -> b
$ Expr -> [((KVar, Expr, GradInfo), SubstV Symbol)]
forall {v}. ExprV v -> [((KVar, ExprV v, GradInfo), 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
_            = []

    go' :: ExprV v -> [((KVar, ExprV v, GradInfo), SubstV v)]
go' (PGrad KVar
k SubstV v
su GradInfo
i ExprV v
e) = [((KVar
k, ExprV v
e, GradInfo
i), SubstV v
su)]
    go' (PAnd [ExprV v]
es)      = (ExprV v -> [((KVar, ExprV v, GradInfo), SubstV v)])
-> [ExprV v] -> [((KVar, ExprV v, GradInfo), SubstV v)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ExprV v -> [((KVar, ExprV v, GradInfo), SubstV v)]
go' [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)

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


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 :: 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 => 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 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
"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
colon Doc -> Doc -> Doc
<+> Doc -> Doc
parens (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. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member KVar
k HashSet KVar
s

instance Semigroup Kuts where
  Kuts
k1 <> :: Kuts -> Kuts -> Kuts
<> Kuts
k2 = HashSet KVar -> Kuts
KS (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]
   -> [BindId]
   -> GInfo SubC a
fi :: forall a.
[SubC a]
-> [WfC a]
-> BindEnv a
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap BindId a
-> Bool
-> Bool
-> [Triggered Expr]
-> AxiomEnv
-> [DataDecl]
-> Tag
-> 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 Tag
ebs
  = FI { cm :: HashMap Integer (SubC a)
cm       = [(Integer, SubC a)] -> HashMap Integer (SubC a)
forall k v. (Eq k, 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.
(Eq k, 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       = (BindId -> BindEnv a -> BindEnv a) -> BindEnv a -> Tag -> BindEnv a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (((Symbol, SortedReft) -> (Symbol, SortedReft))
-> BindId -> BindEnv a -> BindEnv a
forall a.
((Symbol, SortedReft) -> (Symbol, SortedReft))
-> BindId -> BindEnv a -> BindEnv a
adjustBindEnv (Symbol, SortedReft) -> (Symbol, SortedReft)
forall {a}. (a, SortedReft) -> (a, SortedReft)
stripReft) BindEnv a
binds Tag
ebs
       , gLits :: SEnv Sort
gLits    = SEnv Sort
ls
       , dLits :: SEnv Sort
dLits    = SEnv Sort
ds
       , kuts :: Kuts
kuts     = Kuts
ks
       , quals :: [Qualifier]
quals    = [Qualifier]
qs
       , bindInfo :: HashMap BindId a
bindInfo = HashMap BindId a
bi
       , hoInfo :: HOInfo
hoInfo   = Bool -> Bool -> HOInfo
HOI Bool
aHO Bool
aHOq
       , asserts :: [Triggered Expr]
asserts  = [Triggered Expr]
es
       , ae :: AxiomEnv
ae       = AxiomEnv
axe
       , ddecls :: [DataDecl]
ddecls   = [DataDecl]
adts
       , ebinds :: Tag
ebinds   = Tag
ebs
       , lrws :: LocalRewritesEnv
lrws = LocalRewritesEnv
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"
    stripReft :: (a, SortedReft) -> (a, SortedReft)
stripReft (a
sym, SortedReft
reft) = (a
sym, SortedReft
reft { sr_reft = trueReft })

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

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

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

data HOInfo = HOI
  { HOInfo -> Bool
hoBinds :: Bool          -- ^ Allow higher order binds in the environemnt
  , HOInfo -> Bool
hoQuals :: Bool          -- ^ Allow higher order quals
  }
  deriving (HOInfo -> HOInfo -> Bool
(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)               -- ^ Bind  |-> (Symbol, SortedReft)
  , forall (c :: * -> *) a. GInfo c a -> Tag
ebinds   :: ![BindId]                  -- ^ Subset of existential binders
  , forall (c :: * -> *) a. GInfo c a -> SEnv Sort
gLits    :: !(SEnv Sort)               -- ^ Global Constant symbols
  , forall (c :: * -> *) a. GInfo c a -> SEnv Sort
dLits    :: !(SEnv Sort)               -- ^ Distinct Constant symbols
  , forall (c :: * -> *) a. GInfo c a -> Kuts
kuts     :: !Kuts                      -- ^ Set of KVars *not* to eliminate
  , forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals    :: ![Qualifier]               -- ^ Abstract domain
  , forall (c :: * -> *) a. GInfo c a -> HashMap BindId a
bindInfo :: !(M.HashMap BindId a)      -- ^ Metadata about binders
  , forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls   :: ![DataDecl]                -- ^ User-defined data declarations
  , forall (c :: * -> *) a. GInfo c a -> HOInfo
hoInfo   :: !HOInfo                    -- ^ Higher Order info
  , forall (c :: * -> *) a. GInfo c a -> [Triggered Expr]
asserts  :: ![Triggered Expr]          -- ^ TODO: what is this?
  , forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae       :: AxiomEnv                   -- ^ Information about reflected function defs
  , forall (c :: * -> *) a. GInfo c a -> LocalRewritesEnv
lrws     :: LocalRewritesEnv           -- ^ Local rewrites
  }
  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 HasGradual (GInfo c a) where
  isGradual :: GInfo c a -> Bool
isGradual GInfo c a
info = (WfC a -> Bool) -> [WfC a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any WfC a -> Bool
forall a. HasGradual a => a -> Bool
isGradual (HashMap KVar (WfC a) -> [WfC a]
forall k v. HashMap k v -> [v]
M.elems (HashMap KVar (WfC a) -> [WfC a])
-> HashMap KVar (WfC a) -> [WfC a]
forall a b. (a -> b) -> a -> b
$ GInfo c a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws GInfo c a
info)

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

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

instance Semigroup (GInfo c a) where
  GInfo c a
i1 <> :: GInfo c a -> GInfo c a -> GInfo c a
<> GInfo c a
i2 = FI { cm :: HashMap 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
                , ebinds :: Tag
ebinds   = GInfo c a -> Tag
forall (c :: * -> *) a. GInfo c a -> Tag
ebinds GInfo c a
i1   Tag -> Tag -> Tag
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> Tag
forall (c :: * -> *) a. GInfo c a -> Tag
ebinds 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
                }


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
                     , ebinds :: Tag
ebinds   = Tag
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
                     }

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
    (BindEnv a
ubs, EBindEnv a
ebs)    = BindEnv a -> Tag -> (BindEnv a, EBindEnv a)
forall a. BindEnv a -> Tag -> (BindEnv a, EBindEnv a)
splitByQuantifiers (GInfo c a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs GInfo c a
x') (GInfo c a -> Tag
forall (c :: * -> *) a. GInfo c a -> Tag
ebinds GInfo c a
x')
    bindsDoc :: Doc
bindsDoc      = BindEnv a -> Doc
forall a. Fixpoint a => a -> Doc
toFix    BindEnv a
ubs
               Doc -> Doc -> Doc
$++$ EBindEnv a -> Doc
forall a. Fixpoint a => a -> Doc
toFix    EBindEnv a
ebs
    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.
(Eq k, 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.
(Eq k, 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

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

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

---------------------------------------------------------------------------
-- | 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. (Eq k, 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. (Eq k, 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.
(Eq k, 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 NFData AutoRewrite
instance NFData AxiomEnv
instance NFData Rewrite
instance NFData Equation

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. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList []) ([(Integer, [AutoRewrite])] -> HashMap Integer [AutoRewrite]
forall k v. (Eq k, 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

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)

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 :: SubstV Symbol -> Equation -> Equation
subst SubstV Symbol
su = (Expr -> Expr) -> Equation -> Equation
mapEqBody (SubstV Symbol -> Expr -> Expr
forall a. Subable a => 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 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
<+> [Char] -> Doc
text [Char]
" = "
   Doc -> Doc -> Doc
<+> Doc -> Doc
parens (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