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

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

   -- * Serializing
  , toFixpoint
  , writeFInfo
  , saveQuery

   -- * Constructing Queries
  , fi

  -- * Constraints
  , WfC (..), isGWfc, updateWfCExpr
  , SubC, SubcId
  , mkSubC, subcId, sid, senv, 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 (..)

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

import qualified Data.Binary as B
import           Data.Generics             (Data)
#if !MIN_VERSION_base(4,14,0)
import           Data.Semigroup            (Semigroup (..))
#endif

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

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

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

type Tag           = [Int]

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

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

gwInfo :: WfC a -> GWInfo
gwInfo :: 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
_
  = String -> GWInfo
forall a. (?callStack::CallStack) => String -> a
errorstar String
"gwInfo"

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

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

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

instance Loc a => Loc (SimpC a) where 
  srcSpan :: SimpC a -> SrcSpan
srcSpan = 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 :: SInfo a -> [(SubcId, Expr)] -> SInfo a
strengthenHyp SInfo a
si [(SubcId, Expr)]
ies = SInfo a -> HashMap BindId Expr -> SInfo a
forall a. SInfo a -> HashMap BindId Expr -> SInfo a
strengthenBinds SInfo a
si HashMap BindId Expr
bindExprs
  where
    bindExprs :: HashMap BindId Expr
bindExprs        = String -> [(BindId, Expr)] -> HashMap BindId Expr
forall k v.
(?callStack::CallStack, Eq k, Hashable k, Show k) =>
String -> [(k, v)] -> HashMap k v
safeFromList String
"strengthenHyp" [ (SInfo a -> SubcId -> BindId
forall a. SInfo a -> SubcId -> BindId
subcBind SInfo a
si SubcId
i, Expr
e) | (SubcId
i, Expr
e) <- [(SubcId, Expr)]
ies ]

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


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

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, ListNE 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
  sid   :: c a -> Maybe Integer
  stag  :: c a -> Tag
  sinfo :: c a -> a
  clhs  :: BindEnv -> 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
  sid :: SimpC a -> Maybe SubcId
sid       = SimpC a -> Maybe SubcId
forall a. SimpC a -> Maybe SubcId
_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 -> SimpC a -> [(Symbol, SortedReft)]
clhs BindEnv
be SimpC a
c = BindEnv -> IBindEnv -> [(Symbol, SortedReft)]
envCs BindEnv
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
  sid :: SubC a -> Maybe SubcId
sid       = SubC a -> Maybe SubcId
forall a. SubC a -> Maybe SubcId
_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 -> SubC a -> [(Symbol, SortedReft)]
clhs BindEnv
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 -> IBindEnv -> [(Symbol, SortedReft)]
envCs BindEnv
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 :: c a -> SubcId
subcId = String -> Maybe SubcId -> SubcId
forall a. (?callStack::CallStack) => String -> Maybe a -> a
mfromJust String
"subCId" (Maybe SubcId -> SubcId) -> (c a -> Maybe SubcId) -> c a -> SubcId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c a -> Maybe SubcId
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid

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

type GFixSolution = GFixSol Expr

type FixSolution  = M.HashMap KVar Expr

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

toGFixSol :: M.HashMap KVar (e, [e]) -> GFixSol e
toGFixSol :: 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 
  { Result a -> FixResult a
resStatus    :: !(FixResult a)
  , Result a -> FixSolution
resSolution  :: !FixSolution
  , 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
$cto :: forall a x. Rep (Result a) x -> Result a
$cfrom :: forall a x. Result a -> Rep (Result a) x
Generic, BindId -> Result a -> String -> String
[Result a] -> String -> String
Result a -> String
(BindId -> Result a -> String -> String)
-> (Result a -> String)
-> ([Result a] -> String -> String)
-> Show (Result a)
forall a. Show a => BindId -> Result a -> String -> String
forall a. Show a => [Result a] -> String -> String
forall a. Show a => Result a -> String
forall a.
(BindId -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Result a] -> String -> String
$cshowList :: forall a. Show a => [Result a] -> String -> String
show :: Result a -> String
$cshow :: forall a. Show a => Result a -> String
showsPrec :: BindId -> Result a -> String -> String
$cshowsPrec :: forall a. Show a => BindId -> Result a -> String -> String
Show, a -> Result b -> Result a
(a -> b) -> Result a -> Result b
(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
<$ :: a -> Result b -> Result a
$c<$ :: forall a b. a -> Result b -> Result a
fmap :: (a -> b) -> Result a -> Result b
$cfmap :: forall a b. (a -> b) -> Result a -> Result b
Functor)

instance Semigroup (Result a) where
  Result a
r1 <> :: Result a -> Result a -> Result a
<> Result a
r2  = FixResult a -> FixSolution -> GFixSolution -> Result a
forall a. FixResult a -> FixSolution -> GFixSolution -> Result a
Result FixResult a
stat FixSolution
soln 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)
      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 -> GFixSolution -> Result a
forall a. FixResult a -> FixSolution -> GFixSolution -> Result a
Result FixResult a
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 :: Result a
unsafe = Result Any
forall a. Monoid a => a
mempty {resStatus :: FixResult a
resStatus = Stats -> [a] -> FixResult a
forall a. Stats -> [a] -> FixResult a
Unsafe Stats
forall a. Monoid a => a
mempty []}
safe :: Result a
safe   = Result Any
forall a. Monoid a => a
mempty {resStatus :: FixResult a
resStatus = Stats -> FixResult a
forall a. Stats -> FixResult a
Safe Stats
forall a. Monoid a => a
mempty}

isSafe :: Result a -> Bool
isSafe :: Result a -> Bool
isSafe (Result (Safe Stats
_) FixSolution
_ GFixSolution
_) = Bool
True
isSafe Result a
_                     = Bool
False

isUnsafe :: Result a -> Bool
isUnsafe :: 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)     = String -> Doc
text String
"Safe (" Doc -> Doc -> Doc
<+> String -> Doc
text (BindId -> String
forall a. Show a => a -> String
show (BindId -> String) -> BindId -> String
forall a b. (a -> b) -> a -> b
$ Stats -> BindId
Solver.checked Stats
stats) Doc -> Doc -> Doc
<+> Doc
" constraints checked)" 
  -- toFix (UnknownError d) = text $ "Unknown Error: " ++ d
  toFix (Crash [SubC a]
xs String
msg)   = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [ String -> Doc
text String
"Crash!" ] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++  String -> [SubC a] -> [Doc]
forall a. (Ord a, Fixpoint a) => String -> [SubC a] -> [Doc]
pprSinfos String
"CRASH: " [SubC a]
xs [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> Doc
parens (String -> Doc
text String
msg)]
  toFix (Unsafe Stats
_ [SubC a]
xs)    = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Unsafe:" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: String -> [SubC a] -> [Doc]
forall a. (Ord a, Fixpoint a) => String -> [SubC a] -> [Doc]
pprSinfos String
"WARNING: " [SubC a]
xs

pprSinfos :: (Ord a, Fixpoint a) => String -> [SubC a] -> [Doc]
pprSinfos :: String -> [SubC a] -> [Doc]
pprSinfos String
msg = (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> Doc
text String
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 (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 -> String
show = WfC a -> String
forall a. Fixpoint a => a -> String
showFix

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

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

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

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

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

instance Fixpoint a => Fixpoint (SubC a) where
  toFix :: SubC a -> Doc
toFix SubC a
c     = Doc -> BindId -> Doc -> Doc
hang (String -> Doc
text String
"\n\nconstraint:") BindId
2 Doc
bd
     where bd :: Doc
bd =   IBindEnv -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SubC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
c)
              Doc -> Doc -> Doc
$+$ String -> Doc
text String
"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
$+$ String -> Doc
text String
"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 SubcId -> Doc
forall a. Show a => Maybe a -> Doc
pprId (SubC a -> Maybe SubcId
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid SubC a
c) Doc -> Doc -> Doc
<+> String -> Doc
text String
"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 (String -> Doc
text String
"constraint" Doc -> Doc -> Doc
<+> Maybe SubcId -> Doc
forall a. Show a => Maybe a -> Doc
pprId (SubC a -> Maybe SubcId
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid SubC a
c)) (a -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SubC a -> a
forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SubC a
c))

instance Fixpoint a => Fixpoint (SimpC a) where
  toFix :: SimpC a -> Doc
toFix SimpC a
c     = Doc -> BindId -> Doc -> Doc
hang (String -> Doc
text String
"\n\nsimpleConstraint:") BindId
2 Doc
bd
     where bd :: Doc
bd =   IBindEnv -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC a
c)
              Doc -> Doc -> Doc
$+$ String -> Doc
text String
"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 SubcId -> Doc
forall a. Show a => Maybe a -> Doc
pprId (SimpC a -> Maybe SubcId
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid SimpC a
c) Doc -> Doc -> Doc
<+> String -> Doc
text String
"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 (String -> Doc
text String
"simpleConstraint" Doc -> Doc -> Doc
<+> Maybe SubcId -> Doc
forall a. Show a => Maybe a -> Doc
pprId (SimpC a -> Maybe SubcId
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid SimpC a
c)) (a -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SimpC a -> a
forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SimpC a
c))

instance Fixpoint a => Fixpoint (WfC a) where
  toFix :: WfC a -> Doc
toFix WfC a
w     = Doc -> BindId -> Doc -> Doc
hang (String -> Doc
text String
"\n\nwf:") BindId
2 Doc
bd
    where bd :: Doc
bd  =   IBindEnv -> Doc
forall a. Fixpoint a => a -> Doc
toFix (WfC a -> IBindEnv
forall a. WfC a -> IBindEnv
wenv WfC a
w)
              -- NOTE: this next line is printed this way for compatability with the OCAML solver
              Doc -> Doc -> Doc
$+$ String -> Doc
text String
"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 (String -> Doc
text String
"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 (String -> Doc
text String
"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 = String -> Doc
text String
"// META" Doc -> Doc -> Doc
<+> Doc
k Doc -> Doc -> Doc
<+> String -> Doc
text String
":" Doc -> Doc -> Doc
<+> Doc
v

pprId :: Show a => Maybe a -> Doc
pprId :: 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, ListNE 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, ListNE Expr)) -> Doc
pprintTidyGradual Tidy
k ((KVar, (Expr, ListNE Expr)) -> Doc)
-> [(KVar, (Expr, ListNE Expr))] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap KVar (Expr, ListNE Expr) -> [(KVar, (Expr, ListNE Expr))]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap KVar (Expr, ListNE Expr)
xs)

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

ppLocOfKVar :: KVar -> Doc
ppLocOfKVar :: KVar -> Doc
ppLocOfKVar = String -> Doc
text(String -> Doc) -> (KVar -> String) -> KVar -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/=Char
'(') (String -> String) -> (KVar -> String) -> KVar -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> String
symbolString (Symbol -> String) -> (KVar -> Symbol) -> KVar -> String
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 -> String
show = GFixSolution -> String
forall a. PPrint a => a -> String
showpp

----------------------------------------------------------------
instance B.Binary QualPattern 
instance B.Binary QualParam 
instance B.Binary Qualifier
instance B.Binary Kuts
instance B.Binary HOInfo
instance B.Binary GWInfo
instance B.Binary GFixSolution
instance (B.Binary a) => B.Binary (SubC a)
instance (B.Binary a) => B.Binary (WfC a)
instance (B.Binary a) => B.Binary (SimpC a)
instance (B.Binary (c a), B.Binary a) => B.Binary (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


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

wfC :: (Fixpoint a) => IBindEnv -> SortedReft -> a -> [WfC a]
wfC :: 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 String -> [WfC a]
forall a. (?callStack::CallStack) => String -> a
errorstar String
msg
  where
    msg :: String
msg             = String
"wfKvar: malformed wfC " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SortedReft -> String
forall a. Show a => a -> String
show SortedReft
sr String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Subst] -> String
forall a. Show a => a -> String
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 ListNE Expr
es)    = [(KVar
k, Subst
su) | PKVar KVar
k Subst
su <- ListNE 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 ListNE Expr
es)      = (Expr -> [((KVar, Expr, GradInfo), Subst)])
-> ListNE Expr -> [((KVar, Expr, GradInfo), Subst)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [((KVar, Expr, GradInfo), Subst)]
go' ListNE Expr
es
    go' Expr
_              = []

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

subC :: IBindEnv -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> [SubC a]
subC :: IBindEnv
-> SortedReft -> SortedReft -> Maybe SubcId -> Tag -> a -> [SubC a]
subC IBindEnv
γ SortedReft
sr1 SortedReft
sr2 Maybe SubcId
i Tag
y a
z = [IBindEnv
-> SortedReft -> SortedReft -> Maybe SubcId -> Tag -> a -> SubC a
forall a.
IBindEnv
-> SortedReft -> SortedReft -> Maybe SubcId -> Tag -> a -> SubC a
SubC IBindEnv
γ SortedReft
sr1' (Reft -> SortedReft
sr2' Reft
r2') Maybe SubcId
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 SubcId -> Symbol
mkVV Maybe SubcId
i

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

shiftVV :: Reft -> Symbol -> Reft
shiftVV :: Reft -> Symbol -> Reft
shiftVV r :: Reft
r@(Reft (Symbol
v, Expr
ras)) Symbol
v'
   | Symbol
v 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 :: [SubC a] -> [(SubcId, SubC a)]
addIds = (SubcId -> SubC a -> (SubcId, SubC a))
-> [SubcId] -> [SubC a] -> [(SubcId, SubC a)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\SubcId
i SubC a
c -> (SubcId
i, SubcId -> SubC a -> SubC a
forall a a. Show a => a -> SubC a -> SubC a
shiftId SubcId
i (SubC a -> SubC a) -> SubC a -> SubC a
forall a b. (a -> b) -> a -> b
$ SubC a
c {_sid :: Maybe SubcId
_sid = SubcId -> Maybe SubcId
forall a. a -> Maybe a
Just SubcId
i})) [SubcId
1..]
  where 
    -- Adding shiftId to have distinct VV for SMT conversion
    shiftId :: a -> SubC a -> SubC a
shiftId a
i SubC a
c = SubC a
c { slhs :: SortedReft
slhs = a -> SortedReft -> SortedReft
forall a. Show a => a -> SortedReft -> SortedReft
shiftSR a
i (SortedReft -> SortedReft) -> SortedReft -> SortedReft
forall a b. (a -> b) -> a -> b
$ SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
c }
                    { srhs :: SortedReft
srhs = a -> SortedReft -> SortedReft
forall a. Show a => a -> SortedReft -> SortedReft
shiftSR a
i (SortedReft -> SortedReft) -> SortedReft -> SortedReft
forall a b. (a -> b) -> a -> b
$ SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs SubC a
c }
    shiftSR :: a -> SortedReft -> SortedReft
shiftSR a
i SortedReft
sr = SortedReft
sr { sr_reft :: Reft
sr_reft = a -> Reft -> Reft
forall a. Show a => a -> Reft -> Reft
shiftR a
i (Reft -> Reft) -> Reft -> Reft
forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft SortedReft
sr }
    shiftR :: a -> Reft -> Reft
shiftR a
i r :: Reft
r@(Reft (Symbol
v, Expr
_)) = Reft -> Symbol -> Reft
shiftVV Reft
r (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
/= :: Qualifier -> Qualifier -> Bool
$c/= :: Qualifier -> Qualifier -> Bool
== :: Qualifier -> Qualifier -> Bool
$c== :: Qualifier -> Qualifier -> Bool
Eq, BindId -> Qualifier -> String -> String
[Qualifier] -> String -> String
Qualifier -> String
(BindId -> Qualifier -> String -> String)
-> (Qualifier -> String)
-> ([Qualifier] -> String -> String)
-> Show Qualifier
forall a.
(BindId -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Qualifier] -> String -> String
$cshowList :: [Qualifier] -> String -> String
show :: Qualifier -> String
$cshow :: Qualifier -> String
showsPrec :: BindId -> Qualifier -> String -> String
$cshowsPrec :: BindId -> Qualifier -> String -> String
Show, Typeable Qualifier
DataType
Constr
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.
    BindId -> (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 -> DataType
Qualifier -> Constr
(forall b. Data b => b -> b) -> Qualifier -> Qualifier
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Qualifier -> c Qualifier
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Qualifier
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. BindId -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. BindId -> (forall d. Data d => d -> u) -> Qualifier -> u
forall u. (forall d. Data d => d -> u) -> Qualifier -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Qualifier
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Qualifier -> c Qualifier
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Qualifier)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Qualifier)
$cQ :: Constr
$tQualifier :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
gmapMp :: (forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
gmapM :: (forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
gmapQi :: BindId -> (forall d. Data d => d -> u) -> Qualifier -> u
$cgmapQi :: forall u. BindId -> (forall d. Data d => d -> u) -> Qualifier -> u
gmapQ :: (forall d. Data d => d -> u) -> Qualifier -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Qualifier -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
gmapT :: (forall b. Data b => b -> b) -> Qualifier -> Qualifier
$cgmapT :: (forall b. Data b => b -> b) -> Qualifier -> Qualifier
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Qualifier)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Qualifier)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Qualifier)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Qualifier)
dataTypeOf :: Qualifier -> DataType
$cdataTypeOf :: Qualifier -> DataType
toConstr :: Qualifier -> Constr
$ctoConstr :: Qualifier -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Qualifier
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Qualifier
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Qualifier -> c Qualifier
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Qualifier -> c Qualifier
$cp1Data :: Typeable 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
$cto :: forall x. Rep Qualifier x -> Qualifier
$cfrom :: forall x. Qualifier -> Rep Qualifier x
Generic)

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

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

trueQual :: Qualifier
trueQual :: Qualifier
trueQual = Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
Q (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"QTrue" :: String)) [] Expr
forall a. Monoid a => a
mempty (String -> SourcePos
dummyPos String
"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 :: Expr
qBody = Expr -> Expr
f (Qualifier -> Expr
qBody Qualifier
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 BindId
i) = Doc
"as" Doc -> Doc -> Doc
<+> Tidy -> Symbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
s Doc -> Doc -> Doc
<+> (Doc
"$" Doc -> Doc -> Doc
<-> BindId -> Doc
forall a. PPrint a => a -> Doc
pprint BindId
i)
  pprintTidy Tidy
k (PatSuffix BindId
s Symbol
i) = Doc
"as" Doc -> Doc -> Doc
<+> (Doc
"$" Doc -> Doc -> Doc
<-> Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
i) Doc -> Doc -> Doc
<+> Tidy -> BindId -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k BindId
s 
  pprintTidy Tidy
k (PatExact  Symbol
s  ) = Doc
"~"  Doc -> Doc -> Doc
<+> Tidy -> Symbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
s 

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

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

pprQual :: Qualifier -> Doc
pprQual :: Qualifier -> Doc
pprQual (Q Symbol
n [QualParam]
xts Expr
p SourcePos
l) = String -> Doc
text String
"qualif" Doc -> Doc -> Doc
<+> String -> Doc
text (Symbol -> String
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
<+> String -> Doc
text String
"//" 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 -> SubcId -> Maybe (Symbol, Sort))
-> [Symbol] -> [SubcId] -> [Maybe (Symbol, Sort)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (SourcePos
-> SEnv Sort
-> SEnv Sort
-> Symbol
-> SubcId
-> Maybe (Symbol, Sort)
envSort SourcePos
l SEnv Sort
lEnv SEnv Sort
γ) [Symbol]
xs [SubcId
0..]

mkQ :: Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier 
mkQ :: Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier
mkQ Symbol
n = Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
Q Symbol
n ([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
-> SubcId
-> Maybe (Symbol, Sort)
envSort SourcePos
l SEnv Sort
lEnv SEnv Sort
tEnv Symbol
x SubcId
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 -> SubcId -> Symbol
tempSymbol Symbol
"LHTV" SubcId
i
    -- msg = "unknown symbol in qualifier: " ++ show x

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

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

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

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

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

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

-- COPIED from Visitor due to cyclic deps
foldSort' :: (a -> Sort -> a) -> a -> Sort -> a
foldSort' :: (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 (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 (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' a -> Sort -> a
step a
b [Sort
t1, Sort
t2]
    go a
b (FAbs BindId
_ Sort
t)    = a -> Sort -> a
go a
b Sort
t
    go a
b Sort
_             = a
b


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

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

instance Fixpoint Kuts where
  toFix :: Kuts -> Doc
toFix (KS HashSet KVar
s) = [Doc] -> Doc
vcat ([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
<$> 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, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union (Kuts -> HashSet KVar
ksVars Kuts
k1) (Kuts -> HashSet KVar
ksVars Kuts
k2)

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

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

data FInfoWithOpts a = FIO 
  { FInfoWithOpts a -> FInfo a
fioFI   :: FInfo a
  , FInfoWithOpts a -> [String]
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
/= :: HOInfo -> HOInfo -> Bool
$c/= :: HOInfo -> HOInfo -> Bool
== :: HOInfo -> HOInfo -> Bool
$c== :: HOInfo -> HOInfo -> Bool
Eq, BindId -> HOInfo -> String -> String
[HOInfo] -> String -> String
HOInfo -> String
(BindId -> HOInfo -> String -> String)
-> (HOInfo -> String)
-> ([HOInfo] -> String -> String)
-> Show HOInfo
forall a.
(BindId -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [HOInfo] -> String -> String
$cshowList :: [HOInfo] -> String -> String
show :: HOInfo -> String
$cshow :: HOInfo -> String
showsPrec :: BindId -> HOInfo -> String -> String
$cshowsPrec :: BindId -> HOInfo -> String -> String
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
$cto :: forall x. Rep HOInfo x -> HOInfo
$cfrom :: forall x. HOInfo -> Rep HOInfo x
Generic)

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

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


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

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

--------------------------------------------------------------------------
-- | Rendering Queries
--------------------------------------------------------------------------
toFixpoint :: (Fixpoint a, Fixpoint (c a)) => Config -> GInfo c a -> Doc
--------------------------------------------------------------------------
toFixpoint :: 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
$++$ String -> Doc
text String
"\n"
  where
    cfgDoc :: a -> Doc
cfgDoc a
cfg    = String -> Doc
text (String
"// " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
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
. (c a -> Doc) -> [c a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map c a -> Doc
forall a. Fixpoint a => a -> Doc
toFix ([c a] -> [Doc]) -> (GInfo c a -> [c a]) -> GInfo c a -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap SubcId (c a) -> [c a]
forall k v. HashMap k v -> [v]
M.elems (HashMap SubcId (c a) -> [c a])
-> (GInfo c a -> HashMap SubcId (c a)) -> GInfo c a -> [c a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> HashMap SubcId (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (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
. 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 ((String -> Doc
text String
"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
. GInfo c a -> [DataDecl]
forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls
    (BindEnv
ubs, EBindEnv
ebs)    = BindEnv -> Tag -> (BindEnv, EBindEnv)
splitByQuantifiers (GInfo c a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
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 -> Doc
forall a. Fixpoint a => a -> Doc
toFix    BindEnv
ubs
               Doc -> Doc -> Doc
$++$ EBindEnv -> Doc
forall a. Fixpoint a => a -> Doc
toFix    EBindEnv
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
. 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 (String -> Doc
text String
"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
. ((BindId, a) -> Doc) -> [(BindId, a)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (BindId, a) -> Doc
forall a a. (Fixpoint a, Fixpoint a) => (a, a) -> Doc
metaDoc ([(BindId, a)] -> [Doc])
-> (GInfo c a -> [(BindId, a)]) -> GInfo c a -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap BindId a -> [(BindId, a)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap BindId a -> [(BindId, a)])
-> (GInfo c a -> HashMap BindId a) -> GInfo c a -> [(BindId, a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> HashMap BindId a
forall (c :: * -> *) a. GInfo c a -> HashMap BindId a
bindInfo
      | Bool
otherwise = \GInfo c a
_ -> String -> Doc
text String
"\n"

($++$) :: Doc -> Doc -> Doc
Doc
x $++$ :: Doc -> Doc -> Doc
$++$ Doc
y = Doc
x Doc -> Doc -> Doc
$+$ String -> Doc
text String
"\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
. 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 :: Config -> GInfo c a -> String -> IO ()
writeFInfo Config
cfg GInfo c a
fq String
f = String -> String -> IO ()
writeFile String
f (Doc -> String
render (Doc -> String) -> Doc -> String
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 :: FInfo a -> SInfo a
convertFormat FInfo a
fi = FInfo a
fi' { cm :: HashMap SubcId (SimpC a)
cm = BindM -> SubC a -> SimpC a
forall a. BindM -> SubC a -> SimpC a
subcToSimpc BindM
bindm (SubC a -> SimpC a)
-> HashMap SubcId (SubC a) -> HashMap SubcId (SimpC a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FInfo a -> HashMap SubcId (SubC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm FInfo a
fi' }
  where
    (BindM
bindm, FInfo a
fi') = ((BindM, FInfo a) -> SubcId -> SubC a -> (BindM, FInfo a))
-> (BindM, FInfo a) -> HashMap SubcId (SubC a) -> (BindM, FInfo a)
forall a k v. (a -> k -> v -> a) -> a -> HashMap k v -> a
M.foldlWithKey' (BindM, FInfo a) -> SubcId -> SubC a -> (BindM, FInfo a)
forall a. (BindM, FInfo a) -> SubcId -> SubC a -> (BindM, FInfo a)
outVV (BindM
forall k v. HashMap k v
M.empty, FInfo a
fi) (HashMap SubcId (SubC a) -> (BindM, FInfo a))
-> HashMap SubcId (SubC a) -> (BindM, FInfo a)
forall a b. (a -> b) -> a -> b
$ FInfo a -> HashMap SubcId (SubC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm FInfo a
fi

subcToSimpc :: BindM -> SubC a -> SimpC a
subcToSimpc :: BindM -> SubC a -> SimpC a
subcToSimpc BindM
m SubC a
s = SimpC :: forall a.
IBindEnv -> Expr -> Maybe SubcId -> BindId -> Tag -> a -> SimpC a
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 SubcId
_cid        = SubC a -> Maybe SubcId
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid SubC a
s
  , cbind :: BindId
cbind      = String -> SubcId -> BindM -> BindId
forall k v.
(?callStack::CallStack, Eq k, Hashable k) =>
String -> k -> HashMap k v -> v
safeLookup String
"subcToSimpc" (SubC a -> SubcId
forall (c :: * -> *) a. TaggedC c a => c a -> SubcId
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 :: (BindM, FInfo a) -> SubcId -> SubC a -> (BindM, FInfo a)
outVV (BindM
m, FInfo a
fi) SubcId
i SubC a
c = (BindM
m', FInfo a
fi')
  where
    fi' :: FInfo a
fi'           = FInfo a
fi { bs :: BindEnv
bs = BindEnv
be', cm :: HashMap SubcId (SubC a)
cm = HashMap SubcId (SubC a)
cm' }
    m' :: BindM
m'            = SubcId -> BindId -> BindM -> BindM
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert SubcId
i BindId
bId BindM
m
    (BindId
bId, BindEnv
be')    = Symbol -> SortedReft -> BindEnv -> (BindId, BindEnv)
insertBindEnv Symbol
x SortedReft
sr (BindEnv -> (BindId, BindEnv)) -> BindEnv -> (BindId, BindEnv)
forall a b. (a -> b) -> a -> b
$ FInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
bs FInfo a
fi
    cm' :: HashMap SubcId (SubC a)
cm'           = SubcId
-> SubC a -> HashMap SubcId (SubC a) -> HashMap SubcId (SubC a)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert SubcId
i SubC a
c' (HashMap SubcId (SubC a) -> HashMap SubcId (SubC a))
-> HashMap SubcId (SubC a) -> HashMap SubcId (SubC a)
forall a b. (a -> b) -> a -> b
$ FInfo a -> HashMap SubcId (SubC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm FInfo a
fi
    c' :: SubC a
c'            = SubC a
c { _senv :: IBindEnv
_senv = Tag -> IBindEnv -> IBindEnv
insertsIBindEnv [BindId
bId] (IBindEnv -> IBindEnv) -> IBindEnv -> IBindEnv
forall a b. (a -> b) -> a -> b
$ SubC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
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

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

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

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

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

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

instance B.Binary AutoRewrite
instance B.Binary AxiomEnv
instance B.Binary Rewrite
instance B.Binary Equation
instance B.Binary SMTSolver
instance B.Binary Eliminate
instance NFData AutoRewrite
instance NFData AxiomEnv
instance NFData Rewrite
instance NFData Equation
instance NFData SMTSolver
instance NFData Eliminate

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

instance Monoid AxiomEnv where
  mempty :: AxiomEnv
mempty          = [Equation]
-> [Rewrite]
-> HashMap SubcId Bool
-> HashMap SubcId [AutoRewrite]
-> AxiomEnv
AEnv [] [] ([(SubcId, Bool)] -> HashMap SubcId Bool
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList []) ([(SubcId, [AutoRewrite])] -> HashMap SubcId [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
_ = String -> Doc
text (String -> Doc) -> (AxiomEnv -> String) -> AxiomEnv -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AxiomEnv -> String
forall a. Show a => a -> String
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 (Equation -> Equation -> Bool
(Equation -> Equation -> Bool)
-> (Equation -> Equation -> Bool) -> Eq Equation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Equation -> Equation -> Bool
$c/= :: Equation -> Equation -> Bool
== :: Equation -> Equation -> Bool
$c== :: Equation -> Equation -> Bool
Eq, BindId -> Equation -> String -> String
[Equation] -> String -> String
Equation -> String
(BindId -> Equation -> String -> String)
-> (Equation -> String)
-> ([Equation] -> String -> String)
-> Show Equation
forall a.
(BindId -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Equation] -> String -> String
$cshowList :: [Equation] -> String -> String
show :: Equation -> String
$cshow :: Equation -> String
showsPrec :: BindId -> Equation -> String -> String
$cshowsPrec :: BindId -> Equation -> String -> String
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
$cto :: forall x. Rep Equation x -> Equation
$cfrom :: forall x. Equation -> Rep Equation x
Generic)

mkEquation :: Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
mkEquation :: Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
mkEquation Symbol
f [(Symbol, Sort)]
xts Expr
e Sort
out = Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Bool -> Equation
Equ Symbol
f [(Symbol, Sort)]
xts Expr
e Sort
out (Symbol
f Symbol -> [Symbol] -> 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 :: Expr
eqBody = Expr -> Expr
f (Equation -> Expr
eqBody Equation
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 :: [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 (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
/= :: AutoRewrite -> AutoRewrite -> Bool
$c/= :: AutoRewrite -> AutoRewrite -> Bool
== :: AutoRewrite -> AutoRewrite -> Bool
$c== :: AutoRewrite -> AutoRewrite -> Bool
Eq, BindId -> AutoRewrite -> String -> String
[AutoRewrite] -> String -> String
AutoRewrite -> String
(BindId -> AutoRewrite -> String -> String)
-> (AutoRewrite -> String)
-> ([AutoRewrite] -> String -> String)
-> Show AutoRewrite
forall a.
(BindId -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [AutoRewrite] -> String -> String
$cshowList :: [AutoRewrite] -> String -> String
show :: AutoRewrite -> String
$cshow :: AutoRewrite -> String
showsPrec :: BindId -> AutoRewrite -> String -> String
$cshowsPrec :: BindId -> AutoRewrite -> String -> String
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
$cto :: forall x. Rep AutoRewrite x -> AutoRewrite
$cfrom :: forall x. AutoRewrite -> Rep AutoRewrite x
Generic)

instance Hashable SortedReft
instance Hashable AutoRewrite


instance Fixpoint (M.HashMap SubcId [AutoRewrite]) where
  toFix :: HashMap SubcId [AutoRewrite] -> Doc
toFix HashMap SubcId [AutoRewrite]
autoRW =
    [Doc] -> Doc
vcat ((AutoRewrite -> Doc) -> [AutoRewrite] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map AutoRewrite -> Doc
fixRW [AutoRewrite]
rewrites)
    Doc -> Doc -> Doc
$+$ String -> Doc
text String
"rewrite "
    Doc -> Doc -> Doc
<+> [Doc] -> Doc
forall a. Fixpoint a => a -> Doc
toFix [Doc]
rwsMapping
    where
      rewrites :: [AutoRewrite]
rewrites     = [AutoRewrite] -> [AutoRewrite]
forall a. Eq a => [a] -> [a]
L.nub ([AutoRewrite] -> [AutoRewrite]) -> [AutoRewrite] -> [AutoRewrite]
forall a b. (a -> b) -> a -> b
$ ((SubcId, [AutoRewrite]) -> [AutoRewrite])
-> [(SubcId, [AutoRewrite])] -> [AutoRewrite]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SubcId, [AutoRewrite]) -> [AutoRewrite]
forall a b. (a, b) -> b
snd (HashMap SubcId [AutoRewrite] -> [(SubcId, [AutoRewrite])]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap SubcId [AutoRewrite]
autoRW)

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

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



-- eg  SMeasure (f D [x1..xn] e)
-- for f (D x1 .. xn) = e
data Rewrite  = SMeasure
  { Rewrite -> Symbol
smName  :: Symbol         -- eg. f
  , Rewrite -> Symbol
smDC    :: Symbol         -- eg. D
  , Rewrite -> [Symbol]
smArgs  :: [Symbol]       -- eg. xs
  , Rewrite -> Expr
smBody  :: Expr           -- eg. e[xs]
  }
  deriving (Rewrite -> Rewrite -> Bool
(Rewrite -> Rewrite -> Bool)
-> (Rewrite -> Rewrite -> Bool) -> Eq Rewrite
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rewrite -> Rewrite -> Bool
$c/= :: Rewrite -> Rewrite -> Bool
== :: Rewrite -> Rewrite -> Bool
$c== :: Rewrite -> Rewrite -> Bool
Eq, BindId -> Rewrite -> String -> String
[Rewrite] -> String -> String
Rewrite -> String
(BindId -> Rewrite -> String -> String)
-> (Rewrite -> String)
-> ([Rewrite] -> String -> String)
-> Show Rewrite
forall a.
(BindId -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Rewrite] -> String -> String
$cshowList :: [Rewrite] -> String -> String
show :: Rewrite -> String
$cshow :: Rewrite -> String
showsPrec :: BindId -> Rewrite -> String -> String
$cshowsPrec :: BindId -> Rewrite -> String -> String
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
$cto :: forall x. Rep Rewrite x -> Rewrite
$cfrom :: forall x. Rewrite -> Rep Rewrite x
Generic)

instance Fixpoint AxiomEnv where
  toFix :: AxiomEnv -> Doc
toFix AxiomEnv
axe = [Doc] -> Doc
vcat ((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
<$> 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
<$> AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
axe))
              Doc -> Doc -> Doc
$+$ String -> Doc
text String
"expand" Doc -> Doc -> Doc
<+> [Doc] -> Doc
forall a. Fixpoint a => a -> Doc
toFix ((SubcId, Bool) -> Doc
forall a a. (Show a, Show a) => (a, a) -> Doc
pairdoc ((SubcId, Bool) -> Doc) -> [(SubcId, Bool)] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap SubcId Bool -> [(SubcId, Bool)]
forall k v. HashMap k v -> [(k, v)]
M.toList(AxiomEnv -> HashMap SubcId Bool
aenvExpand AxiomEnv
axe))
              Doc -> Doc -> Doc
$+$ HashMap SubcId [AutoRewrite] -> Doc
forall a. Fixpoint a => a -> Doc
toFix (AxiomEnv -> HashMap SubcId [AutoRewrite]
aenvAutoRW AxiomEnv
axe)
    where
      pairdoc :: (a, a) -> Doc
pairdoc (a
x,a
y) = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
y

instance Fixpoint Doc where
  toFix :: Doc -> Doc
toFix = Doc -> Doc
forall a. a -> a
id

instance Fixpoint Equation where
  toFix :: Equation -> Doc
toFix (Equ Symbol
f [(Symbol, Sort)]
xs Expr
e Sort
_ 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
<+> String -> Doc
text String
"=" Doc -> Doc -> Doc
<+> 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)
    = String -> Doc
text String
"match"
   Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
f
   Doc -> Doc -> Doc
<+> Doc -> Doc
parens (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
<+> String -> Doc
text String
" = "
   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