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

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

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

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

   -- * Serializing
  , toFixpoint
  , writeFInfo
  , saveQuery

   -- * Constructing Queries
  , fi

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

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

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

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

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

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

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

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

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

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

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

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

type Tag           = [Int]

data WfC a  =  WfC  { forall a. WfC a -> IBindEnv
wenv  :: !IBindEnv
                    , forall a. WfC a -> (Symbol, Sort, KVar)
wrft  :: (Symbol, Sort, KVar)
                    , forall a. WfC a -> a
winfo :: !a
                    }
             | GWfC { wenv  :: !IBindEnv
                    , wrft  :: !(Symbol, Sort, KVar)
                    , winfo :: !a
                    , forall a. WfC a -> Expr
wexpr :: !Expr
                    , forall a. WfC a -> GradInfo
wloc  :: !GradInfo
                    }
              deriving (WfC a -> WfC a -> Bool
(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 -> Int
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 Int Expr -> SInfo a
forall a. SInfo a -> HashMap Int Expr -> SInfo a
strengthenBinds SInfo a
si HashMap Int Expr
bindExprs
  where
    bindExprs :: HashMap Int Expr
bindExprs        = [Char] -> [(Int, Expr)] -> HashMap Int Expr
forall k v.
(?callStack::CallStack, Eq k, Hashable k, Show k) =>
[Char] -> [(k, v)] -> HashMap k v
safeFromList [Char]
"strengthenHyp" [ (SInfo a -> Integer -> Int
forall a. SInfo a -> Integer -> Int
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 -> Int
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 -> Int
forall a. SimpC a -> Int
cbind SimpC a
c
  | Bool
otherwise
  = [Char] -> Int
forall a. (?callStack::CallStack) => [Char] -> a
errorstar ([Char] -> Int) -> [Char] -> Int
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 Int Expr -> SInfo a
strengthenBinds SInfo a
si HashMap Int Expr
m = SInfo a
si { bs = mapBindEnv f (bs si) }
  where
    f :: Int -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a)
f Int
i (Symbol
x, SortedReft
sr, a
l)   = case Int -> HashMap Int Expr -> Maybe Expr
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Int
i HashMap Int Expr
m of
                         Maybe Expr
Nothing -> (Symbol
x, SortedReft
sr, a
l)
                         Just Expr
e  -> (Symbol
x, SortedReft -> Expr -> SortedReft
strengthenSortedReft SortedReft
sr Expr
e, a
l)

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


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

 -}

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

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

instance TaggedC SimpC a where
  senv :: SimpC a -> IBindEnv
senv      = 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      = Reft -> Expr
reftPred (Reft -> Expr) -> (SubC a -> Reft) -> SubC a -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft (SortedReft -> Reft) -> (SubC a -> SortedReft) -> SubC a -> Reft
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 -> Reft
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, Int -> Result a -> [Char] -> [Char]
[Result a] -> [Char] -> [Char]
Result a -> [Char]
(Int -> Result a -> [Char] -> [Char])
-> (Result a -> [Char])
-> ([Result a] -> [Char] -> [Char])
-> Show (Result a)
forall a. Show a => Int -> Result a -> [Char] -> [Char]
forall a. Show a => [Result a] -> [Char] -> [Char]
forall a. Show a => Result a -> [Char]
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Result a -> [Char] -> [Char]
showsPrec :: Int -> 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 (Int -> [Char]
forall a. Show a => a -> [Char]
show (Int -> [Char]) -> Int -> [Char]
forall a b. (a -> b) -> a -> b
$ Stats -> Int
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 -> Int -> Doc -> Doc
hang ([Char] -> Doc
text [Char]
"\n\nconstraint:") Int
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 -> Int -> Doc -> Doc
hang ([Char] -> Doc
text [Char]
"\n\nsimpleConstraint:") Int
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 -> Int -> Doc -> Doc
hang ([Char] -> Doc
text [Char]
"\n\nwf:") Int
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 -> Reft -> SortedReft
RR Sort
t ((Symbol, Expr) -> Reft
Reft (Symbol
v, KVar -> Subst -> Expr
PKVar KVar
k Subst
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
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 Qualifier
instance NFData Kuts
instance NFData HOInfo
instance NFData GFixSolution
instance NFData GWInfo

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

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

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

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

wfC :: (Fixpoint a) => IBindEnv -> SortedReft -> a -> [WfC a]
wfC :: forall a. Fixpoint a => IBindEnv -> SortedReft -> a -> [WfC a]
wfC IBindEnv
be SortedReft
sr a
x = if (Subst -> Bool) -> [Subst] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Subst -> Bool
isEmptySubst [Subst]
sus -- ++ gsus)
                 -- NV TO RJ This tests fails with [LT:=GHC.Types.LT][EQ:=GHC.Types.EQ][GT:=GHC.Types.GT]]
                 -- NV TO RJ looks like a resolution issue
                then [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]
++ [Subst] -> [Char]
forall a. Show a => a -> [Char]
show ([Subst]
sus [Subst] -> [Subst] -> [Subst]
forall a. [a] -> [a] -> [a]
++ [Subst]
gsus)
    Reft (Symbol
v, Expr
ras)   = SortedReft -> Reft
sr_reft SortedReft
sr
    ([KVar]
ks, [Subst]
sus)       = [(KVar, Subst)] -> ([KVar], [Subst])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(KVar, Subst)] -> ([KVar], [Subst]))
-> [(KVar, Subst)] -> ([KVar], [Subst])
forall a b. (a -> b) -> a -> b
$ Expr -> [(KVar, Subst)]
go Expr
ras
    ([(KVar, Expr, GradInfo)]
gs, [Subst]
gsus)      = [((KVar, Expr, GradInfo), Subst)]
-> ([(KVar, Expr, GradInfo)], [Subst])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((KVar, Expr, GradInfo), Subst)]
 -> ([(KVar, Expr, GradInfo)], [Subst]))
-> [((KVar, Expr, GradInfo), Subst)]
-> ([(KVar, Expr, GradInfo)], [Subst])
forall a b. (a -> b) -> a -> b
$ Expr -> [((KVar, Expr, GradInfo), Subst)]
go' Expr
ras

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

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

mkSubC :: IBindEnv -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a
mkSubC :: forall a.
IBindEnv
-> SortedReft -> SortedReft -> Maybe 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' (Reft -> SortedReft
sr2' Reft
r2') Maybe Integer
i Tag
y a
z | Reft
r2' <- Reft -> [Reft]
reftConjuncts Reft
r2]
   where
     RR Sort
t1 Reft
r1          = SortedReft
sr1
     RR Sort
t2 Reft
r2          = SortedReft
sr2
     sr1' :: SortedReft
sr1'              = Sort -> Reft -> SortedReft
RR Sort
t1 (Reft -> SortedReft) -> Reft -> SortedReft
forall a b. (a -> b) -> a -> b
$ Reft -> Symbol -> Reft
shiftVV Reft
r1  Symbol
vv'
     sr2' :: Reft -> SortedReft
sr2' Reft
r2'          = Sort -> Reft -> SortedReft
RR Sort
t2 (Reft -> SortedReft) -> Reft -> SortedReft
forall a b. (a -> b) -> a -> b
$ Reft -> Symbol -> Reft
shiftVV Reft
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 :: Reft -> Symbol -> Reft
shiftVV r :: Reft
r@(Reft (Symbol
v, Expr
ras)) Symbol
v'
   | Symbol
v Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
v'   = Reft
r
   | Bool
otherwise = (Symbol, Expr) -> Reft
Reft (Symbol
v', Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 Expr
ras (Symbol
v, Symbol -> Expr
EVar Symbol
v'))

addIds :: [SubC a] -> [(Integer, SubC a)]
addIds :: forall a. [SubC a] -> [(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 -> Reft -> Reft
shiftR a
i r :: Reft
r@(Reft (Symbol
v, Expr
_)) = Reft -> Symbol -> Reft
shiftVV Reft
r (Symbol -> a -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
v a
i)

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

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, Int -> QualParam -> [Char] -> [Char]
[QualParam] -> [Char] -> [Char]
QualParam -> [Char]
(Int -> QualParam -> [Char] -> [Char])
-> (QualParam -> [Char])
-> ([QualParam] -> [Char] -> [Char])
-> Show QualParam
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> QualParam -> [Char] -> [Char]
showsPrec :: Int -> 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.
    Int -> (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. Int -> (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. Int -> (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. Int -> (forall d. Data d => d -> u) -> QualParam -> u
gmapQi :: forall u. Int -> (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, Int -> QualPattern -> [Char] -> [Char]
[QualPattern] -> [Char] -> [Char]
QualPattern -> [Char]
(Int -> QualPattern -> [Char] -> [Char])
-> (QualPattern -> [Char])
-> ([QualPattern] -> [Char] -> [Char])
-> Show QualPattern
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> QualPattern -> [Char] -> [Char]
showsPrec :: Int -> 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.
    Int -> (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. Int -> (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. Int -> (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. Int -> (forall d. Data d => d -> u) -> QualPattern -> u
gmapQi :: forall u. Int -> (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)

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

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

instance Subable Qualifier where
  syms :: Qualifier -> [Symbol]
syms   = Qualifier -> [Symbol]
qualFreeSymbols
  subst :: Subst -> Qualifier -> Qualifier
subst  = (Expr -> Expr) -> Qualifier -> Qualifier
mapQualBody ((Expr -> Expr) -> Qualifier -> Qualifier)
-> (Subst -> Expr -> Expr) -> Subst -> Qualifier -> Qualifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> Expr -> Expr
forall a. Subable a => Subst -> 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
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]
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 Int
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
<-> Int -> Doc
forall a. PPrint a => a -> Doc
pprint Int
i)
  pprintTidy Tidy
k (PatSuffix Int
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 -> Int -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Int
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 Qualifier where
  pprintTidy :: Tidy -> Qualifier -> Doc
pprintTidy Tidy
k Qualifier
q = Doc
"qualif" Doc -> Doc -> Doc
<+> Tidy -> Symbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Qualifier -> Symbol
qName Qualifier
q) Doc -> Doc -> Doc
<+> Doc
"defined at" Doc -> Doc -> Doc
<+> Tidy -> SourcePos -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Qualifier -> SourcePos
qPos Qualifier
q)
  -- pprintTidy _ q = pprQual q

pprQual :: Qualifier -> Doc
pprQual :: Qualifier -> Doc
pprQual (Q Symbol
n [QualParam]
xts Expr
p SourcePos
l) = [Char] -> Doc
text [Char]
"qualif" Doc -> Doc -> Doc
<+> [Char] -> Doc
text (Symbol -> [Char]
symbolString Symbol
n) Doc -> Doc -> Doc
<-> Doc -> Doc
parens Doc
args Doc -> Doc -> Doc
<-> Doc
colon Doc -> Doc -> Doc
<+> Doc -> Doc
parens (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
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]
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
mkQual (Qualifier -> Symbol
qName Qualifier
q) (Qualifier -> [QualParam]
qParams Qualifier
q) (Qualifier -> Expr
qBody Qualifier
q) (Qualifier -> SourcePos
qPos Qualifier
q)

-- | constructing qualifiers
mkQual :: Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
mkQual :: Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
mkQual Symbol
n [QualParam]
qps Expr
p = Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
Q Symbol
n [QualParam]
qps' Expr
p
  where
    qps' :: [QualParam]
qps'       = (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, Int)] -> Sort -> Sort
substVars [(Symbol, Int)]
su (Sort -> Sort) -> [Sort] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
ts
  where
    su :: [(Symbol, Int)]
su    = ([Symbol] -> Tag -> [(Symbol, Int)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Int
0..]) ([Symbol] -> [(Symbol, Int)])
-> ([Sort] -> [Symbol]) -> [Sort] -> [(Symbol, Int)]
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, Int)]) -> [Sort] -> [(Symbol, Int)]
forall a b. (a -> b) -> a -> b
$ [Sort]
ts

substVars :: [(Symbol, Int)] -> Sort -> Sort
substVars :: [(Symbol, Int)] -> Sort -> Sort
substVars [(Symbol, Int)]
su = (Sort -> Sort) -> Sort -> Sort
mapSort' Sort -> Sort
tx
  where
    tx :: Sort -> Sort
tx (FObj Symbol
x)
      | Just Int
i <- Symbol -> [(Symbol, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Symbol
x [(Symbol, Int)]
su = Int -> Sort
FVar Int
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 Int
i Sort
t)    = Int -> Sort -> Sort
FAbs Int
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 Int
_ 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, Int -> Kuts -> [Char] -> [Char]
[Kuts] -> [Char] -> [Char]
Kuts -> [Char]
(Int -> Kuts -> [Char] -> [Char])
-> (Kuts -> [Char]) -> ([Kuts] -> [Char] -> [Char]) -> Show Kuts
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> Kuts -> [Char] -> [Char]
showsPrec :: Int -> 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 Int 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 Int 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       = (Int -> 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))
-> Int -> BindEnv a -> BindEnv a
forall a.
((Symbol, SortedReft) -> (Symbol, SortedReft))
-> Int -> 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 Int a
bindInfo = HashMap Int 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
       }
  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, Int -> HOInfo -> [Char] -> [Char]
[HOInfo] -> [Char] -> [Char]
HOInfo -> [Char]
(Int -> HOInfo -> [Char] -> [Char])
-> (HOInfo -> [Char])
-> ([HOInfo] -> [Char] -> [Char])
-> Show HOInfo
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> HOInfo -> [Char] -> [Char]
showsPrec :: Int -> 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)

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 Int a
bindInfo :: !(M.HashMap BindId a)      -- ^ Metadata about binders
  , forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls   :: ![DataDecl]                -- ^ User-defined data declarations
  , forall (c :: * -> *) a. GInfo c a -> HOInfo
hoInfo   :: !HOInfo                    -- ^ Higher Order info
  , forall (c :: * -> *) a. GInfo c a -> [Triggered Expr]
asserts  :: ![Triggered Expr]          -- ^ TODO: what is this?
  , forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae       :: AxiomEnv                   -- ^ Information about reflected function defs
  }
  deriving (GInfo c a -> GInfo c a -> Bool
(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, Int -> GInfo c a -> [Char] -> [Char]
[GInfo c a] -> [Char] -> [Char]
GInfo c a -> [Char]
(Int -> GInfo c a -> [Char] -> [Char])
-> (GInfo c a -> [Char])
-> ([GInfo c a] -> [Char] -> [Char])
-> Show (GInfo c a)
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
Int -> 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)) =>
Int -> GInfo c a -> [Char] -> [Char]
showsPrec :: Int -> 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 Int a
bindInfo = GInfo c a -> HashMap Int a
forall (c :: * -> *) a. GInfo c a -> HashMap Int a
bindInfo GInfo c a
i1 HashMap Int a -> HashMap Int a -> HashMap Int a
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> HashMap Int a
forall (c :: * -> *) a. GInfo c a -> HashMap Int 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
                }


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 Int a
bindInfo = HashMap Int 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
                     }

instance PTable (SInfo a) where
  ptable :: SInfo a -> DocTable
ptable SInfo a
z = [(Doc, Doc)] -> DocTable
DocTable [ ([Char] -> Doc
text [Char]
"# Sub Constraints", Int -> Doc
forall a. PPrint a => a -> Doc
pprint (Int -> Doc) -> Int -> Doc
forall a b. (a -> b) -> a -> b
$ HashMap Integer (SimpC a) -> Int
forall a. HashMap Integer a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (HashMap Integer (SimpC a) -> Int)
-> HashMap Integer (SimpC a) -> Int
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", Int -> Doc
forall a. PPrint a => a -> Doc
pprint (Int -> Doc) -> Int -> Doc
forall a b. (a -> b) -> a -> b
$ HashMap KVar (WfC a) -> Int
forall a. HashMap KVar a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (HashMap KVar (WfC a) -> Int) -> HashMap KVar (WfC a) -> Int
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)) => 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
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
    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
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
. ((Int, a) -> Doc) -> [(Int, a)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int, a) -> Doc
forall {a} {a}. (Fixpoint a, Fixpoint a) => (a, a) -> Doc
metaDoc ([(Int, a)] -> [Doc])
-> (GInfo c a -> [(Int, a)]) -> GInfo c a -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Int a -> [(Int, a)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Int a -> [(Int, a)])
-> (GInfo c a -> HashMap Int a) -> GInfo c a -> [(Int, a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> HashMap Int a
forall (c :: * -> *) a. GInfo c a -> HashMap Int 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)) => 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       = Reft -> Expr
reftPred (Reft -> Expr) -> Reft -> Expr
forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft (SortedReft -> Reft) -> SortedReft -> Reft
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 :: Int
cbind      = [Char] -> Integer -> BindM -> Int
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 -> Int -> BindM -> BindM
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Integer
i Int
bId BindM
m
    (Int
bId, BindEnv a
be')    = Symbol -> SortedReft -> a -> BindEnv a -> (Int, BindEnv a)
forall a.
Symbol -> SortedReft -> a -> BindEnv a -> (Int, 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             = Reft -> Symbol
reftBind (Reft -> Symbol) -> Reft -> Symbol
forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft SortedReft
sr

type BindM = M.HashMap Integer BindId

sinfoToFInfo :: SInfo a -> FInfo a
sinfoToFInfo :: forall a. SInfo a -> FInfo a
sinfoToFInfo SInfo a
fi = SInfo a
fi
  { bs = 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 -> Int -> BindEnv a -> BindEnv a
forall a. Int -> BindEnv a -> BindEnv a
deleteBindEnv (SimpC a -> Int
forall a. SimpC a -> Int
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  = Int -> IBindEnv -> IBindEnv
deleteIBindEnv (SimpC a -> Int
forall a. SimpC a -> Int
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 -> Reft -> SortedReft
RR (SortedReft -> Sort
sr_sort SortedReft
sr) ((Symbol, Expr) -> Reft
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
_) = Int -> BindEnv a -> (Symbol, SortedReft, a)
forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv (SimpC a -> Int
forall a. SimpC a -> Int
cbind SimpC a
s) BindEnv a
env

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

--------------------------------------------------------------------------------
saveQuery :: (Fixpoint a) => Config -> FInfo a -> IO ()
--------------------------------------------------------------------------------
saveQuery :: forall a. Fixpoint a => Config -> FInfo a -> IO ()
saveQuery Config
cfg FInfo a
fi = {- when (save cfg) $ -} do
  let fi' :: FInfo ()
fi'  = 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 :: Config -> FInfo () -> IO ()
saveBinaryQuery :: Config -> FInfo () -> IO ()
saveBinaryQuery Config
cfg FInfo ()
fi = do
  let bfq :: [Char]
bfq  = Ext -> Config -> [Char]
queryFile Ext
Files.BinFq Config
cfg
  [Char] -> IO ()
putStrLn ([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)
  -- B.encodeFile bfq fi

saveTextQuery :: Fixpoint a => Config -> FInfo a -> IO ()
saveTextQuery :: forall a. Fixpoint a => Config -> FInfo a -> IO ()
saveTextQuery Config
cfg FInfo a
fi = do
  let fq :: [Char]
fq   = Ext -> Config -> [Char]
queryFile Ext
Files.Fq Config
cfg
  [Char] -> IO ()
putStrLn ([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] -> [Char] -> IO ()
writeFile [Char]
fq ([Char] -> IO ()) -> [Char] -> IO ()
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, Int -> AxiomEnv -> [Char] -> [Char]
[AxiomEnv] -> [Char] -> [Char]
AxiomEnv -> [Char]
(Int -> AxiomEnv -> [Char] -> [Char])
-> (AxiomEnv -> [Char])
-> ([AxiomEnv] -> [Char] -> [Char])
-> Show AxiomEnv
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> AxiomEnv -> [Char] -> [Char]
showsPrec :: Int -> 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)

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

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

mkEquation :: Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
mkEquation :: Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
mkEquation Symbol
f [(Symbol, Sort)]
xts Expr
e Sort
out = Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Bool -> Equation
Equ Symbol
f [(Symbol, Sort)]
xts Expr
e Sort
out (Symbol
f 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
eqBody Equation
a) -- ++ F.syms (axiomEq a)
  subst :: Subst -> Equation -> Equation
subst Subst
su = (Expr -> Expr) -> Equation -> Equation
mapEqBody (Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
subst Subst
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, Int -> AutoRewrite -> [Char] -> [Char]
[AutoRewrite] -> [Char] -> [Char]
AutoRewrite -> [Char]
(Int -> AutoRewrite -> [Char] -> [Char])
-> (AutoRewrite -> [Char])
-> ([AutoRewrite] -> [Char] -> [Char])
-> Show AutoRewrite
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> AutoRewrite -> [Char] -> [Char]
showsPrec :: Int -> 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]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (AutoRewrite -> Int
forall a. Hashable a => a -> Int
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]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (AutoRewrite -> Int
forall a. Hashable a => a -> Int
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. Int -> (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. Int -> (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. Int -> (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. Int -> (forall d. Data d => d -> u) -> Rewrite -> u
gmapQi :: forall u. Int -> (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, Int -> Rewrite -> [Char] -> [Char]
[Rewrite] -> [Char] -> [Char]
Rewrite -> [Char]
(Int -> Rewrite -> [Char] -> [Char])
-> (Rewrite -> [Char])
-> ([Rewrite] -> [Char] -> [Char])
-> Show Rewrite
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> Rewrite -> [Char] -> [Char]
showsPrec :: Int -> 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 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