{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternGuards #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}
module Language.Fixpoint.Types.Constraints (
FInfo, SInfo, GInfo (..), FInfoWithOpts(..)
, convertFormat
, sinfoToFInfo
, Solver
, toFixpoint
, writeFInfo
, saveQuery
, fi
, WfC (..), isGWfc, updateWfCExpr
, SubC, SubcId
, mkSubC, subcId, sid, senv, updateSEnv, slhs, srhs, stag, subC, wfC
, SimpC (..)
, Tag
, TaggedC, clhs, crhs
, strengthenHyp
, strengthenBinds
, addIds
, sinfo
, shiftVV
, gwInfo, GWInfo (..)
, Qualifier (..)
, QualParam (..)
, QualPattern (..)
, trueQual
, qualifier
, mkQual
, remakeQual
, mkQ
, qualBinds
, FixSolution
, GFixSolution, toGFixSol
, Result (..)
, unsafe, isUnsafe, isSafe ,safe
, Kuts (..)
, ksMember
, HOInfo (..)
, allowHO
, allowHOquals
, AxiomEnv (..)
, Equation (..)
, mkEquation
, Rewrite (..)
, AutoRewrite (..)
, dedupAutoRewrites
, substVars
, sortVars
, gSorts
) where
import qualified Data.Store as S
import Data.Generics (Data)
import Data.Aeson hiding (Result)
import qualified Data.Set as Set
import Data.Typeable (Typeable)
import Data.Hashable
import GHC.Generics (Generic)
import qualified Data.List as L
import Data.Maybe (catMaybes)
import Control.DeepSeq
import Control.Monad (void)
import Language.Fixpoint.Types.PrettyPrint
import Language.Fixpoint.Types.Config hiding (allowHO)
import Language.Fixpoint.Types.Triggers
import Language.Fixpoint.Types.Names
import Language.Fixpoint.Types.Errors
import Language.Fixpoint.Types.Spans
import Language.Fixpoint.Types.Sorts
import Language.Fixpoint.Types.Refinements
import Language.Fixpoint.Types.Substitutions
import Language.Fixpoint.Types.Environments
import qualified Language.Fixpoint.Utils.Files as Files
import qualified Language.Fixpoint.Solver.Stats as Solver
import Language.Fixpoint.Misc
import Text.PrettyPrint.HughesPJ.Compat
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import qualified Data.ByteString as B
import qualified Data.Binary as B
type Tag = [Int]
data WfC a = WfC { forall a. WfC a -> IBindEnv
wenv :: !IBindEnv
, forall a. WfC a -> (Symbol, Sort, KVar)
wrft :: (Symbol, Sort, KVar)
, forall a. WfC a -> a
winfo :: !a
}
| GWfC { wenv :: !IBindEnv
, wrft :: !(Symbol, Sort, KVar)
, winfo :: !a
, forall a. WfC a -> Expr
wexpr :: !Expr
, forall a. WfC a -> GradInfo
wloc :: !GradInfo
}
deriving (WfC a -> WfC a -> Bool
(WfC a -> WfC a -> Bool) -> (WfC a -> WfC a -> Bool) -> Eq (WfC a)
forall a. Eq a => WfC a -> WfC a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => WfC a -> WfC a -> Bool
== :: WfC a -> WfC a -> Bool
$c/= :: forall a. Eq a => WfC a -> WfC a -> Bool
/= :: WfC a -> WfC a -> Bool
Eq, (forall x. WfC a -> Rep (WfC a) x)
-> (forall x. Rep (WfC a) x -> WfC a) -> Generic (WfC a)
forall x. Rep (WfC a) x -> WfC a
forall x. WfC a -> Rep (WfC a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (WfC a) x -> WfC a
forall a x. WfC a -> Rep (WfC a) x
$cfrom :: forall a x. WfC a -> Rep (WfC a) x
from :: forall x. WfC a -> Rep (WfC a) x
$cto :: forall a x. Rep (WfC a) x -> WfC a
to :: forall x. Rep (WfC a) x -> WfC a
Generic, (forall a b. (a -> b) -> WfC a -> WfC b)
-> (forall a b. a -> WfC b -> WfC a) -> Functor WfC
forall a b. a -> WfC b -> WfC a
forall a b. (a -> b) -> WfC a -> WfC b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> WfC a -> WfC b
fmap :: forall a b. (a -> b) -> WfC a -> WfC b
$c<$ :: forall a b. a -> WfC b -> WfC a
<$ :: forall a b. a -> WfC b -> WfC a
Functor)
data GWInfo = GWInfo { GWInfo -> Symbol
gsym :: Symbol
, GWInfo -> Sort
gsort :: Sort
, GWInfo -> Expr
gexpr :: Expr
, GWInfo -> GradInfo
ginfo :: GradInfo
}
deriving (GWInfo -> GWInfo -> Bool
(GWInfo -> GWInfo -> Bool)
-> (GWInfo -> GWInfo -> Bool) -> Eq GWInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: GWInfo -> GWInfo -> Bool
== :: GWInfo -> GWInfo -> Bool
$c/= :: GWInfo -> GWInfo -> Bool
/= :: GWInfo -> GWInfo -> Bool
Eq, (forall x. GWInfo -> Rep GWInfo x)
-> (forall x. Rep GWInfo x -> GWInfo) -> Generic GWInfo
forall x. Rep GWInfo x -> GWInfo
forall x. GWInfo -> Rep GWInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. GWInfo -> Rep GWInfo x
from :: forall x. GWInfo -> Rep GWInfo x
$cto :: forall x. Rep GWInfo x -> GWInfo
to :: forall x. Rep GWInfo x -> GWInfo
Generic)
gwInfo :: WfC a -> GWInfo
gwInfo :: forall a. WfC a -> GWInfo
gwInfo (GWfC IBindEnv
_ (Symbol
x,Sort
s,KVar
_) a
_ Expr
e GradInfo
i)
= Symbol -> Sort -> Expr -> GradInfo -> GWInfo
GWInfo Symbol
x Sort
s Expr
e GradInfo
i
gwInfo WfC a
_
= [Char] -> GWInfo
forall a. (?callStack::CallStack) => [Char] -> a
errorstar [Char]
"gwInfo"
updateWfCExpr :: (Expr -> Expr) -> WfC a -> WfC a
updateWfCExpr :: forall a. (Expr -> Expr) -> WfC a -> WfC a
updateWfCExpr Expr -> Expr
_ w :: WfC a
w@WfC{} = WfC a
w
updateWfCExpr Expr -> Expr
f w :: WfC a
w@GWfC{} = WfC a
w{wexpr = f (wexpr w)}
isGWfc :: WfC a -> Bool
isGWfc :: forall a. WfC a -> Bool
isGWfc GWfC{} = Bool
True
isGWfc WfC{} = Bool
False
instance HasGradual (WfC a) where
isGradual :: WfC a -> Bool
isGradual = WfC a -> Bool
forall a. WfC a -> Bool
isGWfc
type SubcId = Integer
data SubC a = SubC
{ forall a. SubC a -> IBindEnv
_senv :: !IBindEnv
, forall a. SubC a -> SortedReft
slhs :: !SortedReft
, forall a. SubC a -> SortedReft
srhs :: !SortedReft
, forall a. SubC a -> Maybe Integer
_sid :: !(Maybe SubcId)
, forall a. SubC a -> Tag
_stag :: !Tag
, forall a. SubC a -> a
_sinfo :: !a
}
deriving (SubC a -> SubC a -> Bool
(SubC a -> SubC a -> Bool)
-> (SubC a -> SubC a -> Bool) -> Eq (SubC a)
forall a. Eq a => SubC a -> SubC a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => SubC a -> SubC a -> Bool
== :: SubC a -> SubC a -> Bool
$c/= :: forall a. Eq a => SubC a -> SubC a -> Bool
/= :: SubC a -> SubC a -> Bool
Eq, (forall x. SubC a -> Rep (SubC a) x)
-> (forall x. Rep (SubC a) x -> SubC a) -> Generic (SubC a)
forall x. Rep (SubC a) x -> SubC a
forall x. SubC a -> Rep (SubC a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (SubC a) x -> SubC a
forall a x. SubC a -> Rep (SubC a) x
$cfrom :: forall a x. SubC a -> Rep (SubC a) x
from :: forall x. SubC a -> Rep (SubC a) x
$cto :: forall a x. Rep (SubC a) x -> SubC a
to :: forall x. Rep (SubC a) x -> SubC a
Generic, (forall a b. (a -> b) -> SubC a -> SubC b)
-> (forall a b. a -> SubC b -> SubC a) -> Functor SubC
forall a b. a -> SubC b -> SubC a
forall a b. (a -> b) -> SubC a -> SubC b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> SubC a -> SubC b
fmap :: forall a b. (a -> b) -> SubC a -> SubC b
$c<$ :: forall a b. a -> SubC b -> SubC a
<$ :: forall a b. a -> SubC b -> SubC a
Functor)
data SimpC a = SimpC
{ forall a. SimpC a -> IBindEnv
_cenv :: !IBindEnv
, forall a. SimpC a -> Expr
_crhs :: !Expr
, forall a. SimpC a -> Maybe Integer
_cid :: !(Maybe Integer)
, forall a. SimpC a -> Int
cbind :: !BindId
, forall a. SimpC a -> Tag
_ctag :: !Tag
, forall a. SimpC a -> a
_cinfo :: !a
}
deriving ((forall x. SimpC a -> Rep (SimpC a) x)
-> (forall x. Rep (SimpC a) x -> SimpC a) -> Generic (SimpC a)
forall x. Rep (SimpC a) x -> SimpC a
forall x. SimpC a -> Rep (SimpC a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (SimpC a) x -> SimpC a
forall a x. SimpC a -> Rep (SimpC a) x
$cfrom :: forall a x. SimpC a -> Rep (SimpC a) x
from :: forall x. SimpC a -> Rep (SimpC a) x
$cto :: forall a x. Rep (SimpC a) x -> SimpC a
to :: forall x. Rep (SimpC a) x -> SimpC a
Generic, (forall a b. (a -> b) -> SimpC a -> SimpC b)
-> (forall a b. a -> SimpC b -> SimpC a) -> Functor SimpC
forall a b. a -> SimpC b -> SimpC a
forall a b. (a -> b) -> SimpC a -> SimpC b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> SimpC a -> SimpC b
fmap :: forall a b. (a -> b) -> SimpC a -> SimpC b
$c<$ :: forall a b. a -> SimpC b -> SimpC a
<$ :: forall a b. a -> SimpC b -> SimpC a
Functor)
instance Loc a => Loc (SimpC a) where
srcSpan :: SimpC a -> SrcSpan
srcSpan = a -> SrcSpan
forall a. Loc a => a -> SrcSpan
srcSpan (a -> SrcSpan) -> (SimpC a -> a) -> SimpC a -> SrcSpan
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpC a -> a
forall a. SimpC a -> a
_cinfo
strengthenHyp :: SInfo a -> [(Integer, Expr)] -> SInfo a
strengthenHyp :: forall a. SInfo a -> [(Integer, Expr)] -> SInfo a
strengthenHyp SInfo a
si [(Integer, Expr)]
ies = SInfo a -> HashMap Int Expr -> SInfo a
forall a. SInfo a -> HashMap Int Expr -> SInfo a
strengthenBinds SInfo a
si HashMap Int Expr
bindExprs
where
bindExprs :: HashMap Int Expr
bindExprs = [Char] -> [(Int, Expr)] -> HashMap Int Expr
forall k v.
(?callStack::CallStack, Eq k, Hashable k, Show k) =>
[Char] -> [(k, v)] -> HashMap k v
safeFromList [Char]
"strengthenHyp" [ (SInfo a -> Integer -> Int
forall a. SInfo a -> Integer -> Int
subcBind SInfo a
si Integer
i, Expr
e) | (Integer
i, Expr
e) <- [(Integer, Expr)]
ies ]
subcBind :: SInfo a -> SubcId -> BindId
subcBind :: forall a. SInfo a -> Integer -> Int
subcBind SInfo a
si Integer
i
| Just SimpC a
c <- Integer -> HashMap Integer (SimpC a) -> Maybe (SimpC a)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Integer
i (SInfo a -> HashMap Integer (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm SInfo a
si)
= SimpC a -> Int
forall a. SimpC a -> Int
cbind SimpC a
c
| Bool
otherwise
= [Char] -> Int
forall a. (?callStack::CallStack) => [Char] -> a
errorstar ([Char] -> Int) -> [Char] -> Int
forall a b. (a -> b) -> a -> b
$ [Char]
"Unknown subcId in subcBind: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
i
strengthenBinds :: SInfo a -> M.HashMap BindId Expr -> SInfo a
strengthenBinds :: forall a. SInfo a -> HashMap Int Expr -> SInfo a
strengthenBinds SInfo a
si HashMap Int Expr
m = SInfo a
si { bs = mapBindEnv f (bs si) }
where
f :: Int -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a)
f Int
i (Symbol
x, SortedReft
sr, a
l) = case Int -> HashMap Int Expr -> Maybe Expr
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Int
i HashMap Int Expr
m of
Maybe Expr
Nothing -> (Symbol
x, SortedReft
sr, a
l)
Just Expr
e -> (Symbol
x, SortedReft -> Expr -> SortedReft
strengthenSortedReft SortedReft
sr Expr
e, a
l)
strengthenSortedReft :: SortedReft -> Expr -> SortedReft
strengthenSortedReft :: SortedReft -> Expr -> SortedReft
strengthenSortedReft (RR Sort
s (Reft (Symbol
v, Expr
r))) Expr
e = Sort -> Reft -> SortedReft
RR Sort
s ((Symbol, Expr) -> Reft
Reft (Symbol
v, [Expr] -> Expr
pAnd [Expr
r, Expr
e]))
class TaggedC c a where
senv :: c a -> IBindEnv
updateSEnv :: c a -> (IBindEnv -> IBindEnv) -> c a
sid :: c a -> Maybe Integer
stag :: c a -> Tag
sinfo :: c a -> a
clhs :: BindEnv a -> c a -> [(Symbol, SortedReft)]
crhs :: c a -> Expr
instance TaggedC SimpC a where
senv :: SimpC a -> IBindEnv
senv = SimpC a -> IBindEnv
forall a. SimpC a -> IBindEnv
_cenv
updateSEnv :: SimpC a -> (IBindEnv -> IBindEnv) -> SimpC a
updateSEnv SimpC a
c IBindEnv -> IBindEnv
f = SimpC a
c { _cenv = f (_cenv c) }
sid :: SimpC a -> Maybe Integer
sid = SimpC a -> Maybe Integer
forall a. SimpC a -> Maybe Integer
_cid
stag :: SimpC a -> Tag
stag = SimpC a -> Tag
forall a. SimpC a -> Tag
_ctag
sinfo :: SimpC a -> a
sinfo = SimpC a -> a
forall a. SimpC a -> a
_cinfo
crhs :: SimpC a -> Expr
crhs = SimpC a -> Expr
forall a. SimpC a -> Expr
_crhs
clhs :: BindEnv a -> SimpC a -> [(Symbol, SortedReft)]
clhs BindEnv a
be SimpC a
c = BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
envCs BindEnv a
be (SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC a
c)
instance TaggedC SubC a where
senv :: SubC a -> IBindEnv
senv = SubC a -> IBindEnv
forall a. SubC a -> IBindEnv
_senv
updateSEnv :: SubC a -> (IBindEnv -> IBindEnv) -> SubC a
updateSEnv SubC a
c IBindEnv -> IBindEnv
f = SubC a
c { _senv = f (_senv c) }
sid :: SubC a -> Maybe Integer
sid = SubC a -> Maybe Integer
forall a. SubC a -> Maybe Integer
_sid
stag :: SubC a -> Tag
stag = SubC a -> Tag
forall a. SubC a -> Tag
_stag
sinfo :: SubC a -> a
sinfo = SubC a -> a
forall a. SubC a -> a
_sinfo
crhs :: SubC a -> Expr
crhs = Reft -> Expr
reftPred (Reft -> Expr) -> (SubC a -> Reft) -> SubC a -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft (SortedReft -> Reft) -> (SubC a -> SortedReft) -> SubC a -> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs
clhs :: BindEnv a -> SubC a -> [(Symbol, SortedReft)]
clhs BindEnv a
be SubC a
c = SortedReft -> (Symbol, SortedReft)
sortedReftBind (SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
c) (Symbol, SortedReft)
-> [(Symbol, SortedReft)] -> [(Symbol, SortedReft)]
forall a. a -> [a] -> [a]
: BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
envCs BindEnv a
be (SubC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
c)
sortedReftBind :: SortedReft -> (Symbol, SortedReft)
sortedReftBind :: SortedReft -> (Symbol, SortedReft)
sortedReftBind SortedReft
sr = (Symbol
x, SortedReft
sr)
where
Reft (Symbol
x, Expr
_) = SortedReft -> Reft
sr_reft SortedReft
sr
subcId :: (TaggedC c a) => c a -> SubcId
subcId :: forall (c :: * -> *) a. TaggedC c a => c a -> Integer
subcId = [Char] -> Maybe Integer -> Integer
forall a. (?callStack::CallStack) => [Char] -> Maybe a -> a
mfromJust [Char]
"subCId" (Maybe Integer -> Integer)
-> (c a -> Maybe Integer) -> c a -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
sid
type GFixSolution = GFixSol Expr
type FixSolution = M.HashMap KVar Expr
newtype GFixSol e = GSol (M.HashMap KVar (e, [e]))
deriving ((forall x. GFixSol e -> Rep (GFixSol e) x)
-> (forall x. Rep (GFixSol e) x -> GFixSol e)
-> Generic (GFixSol e)
forall x. Rep (GFixSol e) x -> GFixSol e
forall x. GFixSol e -> Rep (GFixSol e) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (GFixSol e) x -> GFixSol e
forall e x. GFixSol e -> Rep (GFixSol e) x
$cfrom :: forall e x. GFixSol e -> Rep (GFixSol e) x
from :: forall x. GFixSol e -> Rep (GFixSol e) x
$cto :: forall e x. Rep (GFixSol e) x -> GFixSol e
to :: forall x. Rep (GFixSol e) x -> GFixSol e
Generic, NonEmpty (GFixSol e) -> GFixSol e
GFixSol e -> GFixSol e -> GFixSol e
(GFixSol e -> GFixSol e -> GFixSol e)
-> (NonEmpty (GFixSol e) -> GFixSol e)
-> (forall b. Integral b => b -> GFixSol e -> GFixSol e)
-> Semigroup (GFixSol e)
forall b. Integral b => b -> GFixSol e -> GFixSol e
forall e. NonEmpty (GFixSol e) -> GFixSol e
forall e. GFixSol e -> GFixSol e -> GFixSol e
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall e b. Integral b => b -> GFixSol e -> GFixSol e
$c<> :: forall e. GFixSol e -> GFixSol e -> GFixSol e
<> :: GFixSol e -> GFixSol e -> GFixSol e
$csconcat :: forall e. NonEmpty (GFixSol e) -> GFixSol e
sconcat :: NonEmpty (GFixSol e) -> GFixSol e
$cstimes :: forall e b. Integral b => b -> GFixSol e -> GFixSol e
stimes :: forall b. Integral b => b -> GFixSol e -> GFixSol e
Semigroup, Semigroup (GFixSol e)
GFixSol e
Semigroup (GFixSol e) =>
GFixSol e
-> (GFixSol e -> GFixSol e -> GFixSol e)
-> ([GFixSol e] -> GFixSol e)
-> Monoid (GFixSol e)
[GFixSol e] -> GFixSol e
GFixSol e -> GFixSol e -> GFixSol e
forall e. Semigroup (GFixSol e)
forall e. GFixSol e
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall e. [GFixSol e] -> GFixSol e
forall e. GFixSol e -> GFixSol e -> GFixSol e
$cmempty :: forall e. GFixSol e
mempty :: GFixSol e
$cmappend :: forall e. GFixSol e -> GFixSol e -> GFixSol e
mappend :: GFixSol e -> GFixSol e -> GFixSol e
$cmconcat :: forall e. [GFixSol e] -> GFixSol e
mconcat :: [GFixSol e] -> GFixSol e
Monoid, (forall a b. (a -> b) -> GFixSol a -> GFixSol b)
-> (forall a b. a -> GFixSol b -> GFixSol a) -> Functor GFixSol
forall a b. a -> GFixSol b -> GFixSol a
forall a b. (a -> b) -> GFixSol a -> GFixSol b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> GFixSol a -> GFixSol b
fmap :: forall a b. (a -> b) -> GFixSol a -> GFixSol b
$c<$ :: forall a b. a -> GFixSol b -> GFixSol a
<$ :: forall a b. a -> GFixSol b -> GFixSol a
Functor)
toGFixSol :: M.HashMap KVar (e, [e]) -> GFixSol e
toGFixSol :: forall e. HashMap KVar (e, [e]) -> GFixSol e
toGFixSol = HashMap KVar (e, [e]) -> GFixSol e
forall e. HashMap KVar (e, [e]) -> GFixSol e
GSol
data Result a = Result
{ forall a. Result a -> FixResult a
resStatus :: !(FixResult a)
, forall a. Result a -> FixSolution
resSolution :: !FixSolution
, forall a. Result a -> FixSolution
resNonCutsSolution :: !FixSolution
, forall a. Result a -> GFixSolution
gresSolution :: !GFixSolution
}
deriving ((forall x. Result a -> Rep (Result a) x)
-> (forall x. Rep (Result a) x -> Result a) -> Generic (Result a)
forall x. Rep (Result a) x -> Result a
forall x. Result a -> Rep (Result a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Result a) x -> Result a
forall a x. Result a -> Rep (Result a) x
$cfrom :: forall a x. Result a -> Rep (Result a) x
from :: forall x. Result a -> Rep (Result a) x
$cto :: forall a x. Rep (Result a) x -> Result a
to :: forall x. Rep (Result a) x -> Result a
Generic, Int -> Result a -> [Char] -> [Char]
[Result a] -> [Char] -> [Char]
Result a -> [Char]
(Int -> Result a -> [Char] -> [Char])
-> (Result a -> [Char])
-> ([Result a] -> [Char] -> [Char])
-> Show (Result a)
forall a. Show a => Int -> Result a -> [Char] -> [Char]
forall a. Show a => [Result a] -> [Char] -> [Char]
forall a. Show a => Result a -> [Char]
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Result a -> [Char] -> [Char]
showsPrec :: Int -> Result a -> [Char] -> [Char]
$cshow :: forall a. Show a => Result a -> [Char]
show :: Result a -> [Char]
$cshowList :: forall a. Show a => [Result a] -> [Char] -> [Char]
showList :: [Result a] -> [Char] -> [Char]
Show, (forall a b. (a -> b) -> Result a -> Result b)
-> (forall a b. a -> Result b -> Result a) -> Functor Result
forall a b. a -> Result b -> Result a
forall a b. (a -> b) -> Result a -> Result b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Result a -> Result b
fmap :: forall a b. (a -> b) -> Result a -> Result b
$c<$ :: forall a b. a -> Result b -> Result a
<$ :: forall a b. a -> Result b -> Result a
Functor)
instance ToJSON a => ToJSON (Result a) where
toJSON :: Result a -> Value
toJSON = FixResult a -> Value
forall a. ToJSON a => a -> Value
toJSON (FixResult a -> Value)
-> (Result a -> FixResult a) -> Result a -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result a -> FixResult a
forall a. Result a -> FixResult a
resStatus
instance Semigroup (Result a) where
Result a
r1 <> :: Result a -> Result a -> Result a
<> Result a
r2 = FixResult a
-> FixSolution -> FixSolution -> GFixSolution -> Result a
forall a.
FixResult a
-> FixSolution -> FixSolution -> GFixSolution -> Result a
Result FixResult a
stat FixSolution
soln FixSolution
nonCutsSoln GFixSolution
gsoln
where
stat :: FixResult a
stat = Result a -> FixResult a
forall a. Result a -> FixResult a
resStatus Result a
r1 FixResult a -> FixResult a -> FixResult a
forall a. Semigroup a => a -> a -> a
<> Result a -> FixResult a
forall a. Result a -> FixResult a
resStatus Result a
r2
soln :: FixSolution
soln = Result a -> FixSolution
forall a. Result a -> FixSolution
resSolution Result a
r1 FixSolution -> FixSolution -> FixSolution
forall a. Semigroup a => a -> a -> a
<> Result a -> FixSolution
forall a. Result a -> FixSolution
resSolution Result a
r2
nonCutsSoln :: FixSolution
nonCutsSoln = Result a -> FixSolution
forall a. Result a -> FixSolution
resNonCutsSolution Result a
r1 FixSolution -> FixSolution -> FixSolution
forall a. Semigroup a => a -> a -> a
<> Result a -> FixSolution
forall a. Result a -> FixSolution
resNonCutsSolution Result a
r2
gsoln :: GFixSolution
gsoln = Result a -> GFixSolution
forall a. Result a -> GFixSolution
gresSolution Result a
r1 GFixSolution -> GFixSolution -> GFixSolution
forall a. Semigroup a => a -> a -> a
<> Result a -> GFixSolution
forall a. Result a -> GFixSolution
gresSolution Result a
r2
instance Monoid (Result a) where
mempty :: Result a
mempty = FixResult a
-> FixSolution -> FixSolution -> GFixSolution -> Result a
forall a.
FixResult a
-> FixSolution -> FixSolution -> GFixSolution -> Result a
Result FixResult a
forall a. Monoid a => a
mempty FixSolution
forall a. Monoid a => a
mempty FixSolution
forall a. Monoid a => a
mempty GFixSolution
forall a. Monoid a => a
mempty
mappend :: Result a -> Result a -> Result a
mappend = Result a -> Result a -> Result a
forall a. Semigroup a => a -> a -> a
(<>)
unsafe, safe :: Result a
unsafe :: forall a. Result a
unsafe = Result Any
forall a. Monoid a => a
mempty {resStatus = Unsafe mempty []}
safe :: forall a. Result a
safe = Result Any
forall a. Monoid a => a
mempty {resStatus = Safe mempty}
isSafe :: Result a -> Bool
isSafe :: forall a. Result a -> Bool
isSafe Result a
r = case Result a -> FixResult a
forall a. Result a -> FixResult a
resStatus Result a
r of
Safe{} -> Bool
True
FixResult a
_ -> Bool
False
isUnsafe :: Result a -> Bool
isUnsafe :: forall a. Result a -> Bool
isUnsafe Result a
r | Unsafe Stats
_ [a]
_ <- Result a -> FixResult a
forall a. Result a -> FixResult a
resStatus Result a
r
= Bool
True
isUnsafe Result a
_ = Bool
False
instance (Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a)) where
toFix :: FixResult (SubC a) -> Doc
toFix (Safe Stats
stats) = [Char] -> Doc
text [Char]
"Safe (" Doc -> Doc -> Doc
<+> [Char] -> Doc
text (Int -> [Char]
forall a. Show a => a -> [Char]
show (Int -> [Char]) -> Int -> [Char]
forall a b. (a -> b) -> a -> b
$ Stats -> Int
Solver.checked Stats
stats) Doc -> Doc -> Doc
<+> Doc
" constraints checked)"
toFix (Crash [(SubC a, Maybe [Char])]
xs [Char]
msg) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [ [Char] -> Doc
text [Char]
"Crash!" ] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [SubC a] -> [Doc]
forall a. (Ord a, Fixpoint a) => [Char] -> [SubC a] -> [Doc]
pprSinfos [Char]
"CRASH: " ((SubC a, Maybe [Char]) -> SubC a
forall a b. (a, b) -> a
fst ((SubC a, Maybe [Char]) -> SubC a)
-> [(SubC a, Maybe [Char])] -> [SubC a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SubC a, Maybe [Char])]
xs) [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> Doc
parens ([Char] -> Doc
text [Char]
msg)]
toFix (Unsafe Stats
_ [SubC a]
xs) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
text [Char]
"Unsafe:" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Char] -> [SubC a] -> [Doc]
forall a. (Ord a, Fixpoint a) => [Char] -> [SubC a] -> [Doc]
pprSinfos [Char]
"WARNING: " [SubC a]
xs
pprSinfos :: (Ord a, Fixpoint a) => String -> [SubC a] -> [Doc]
pprSinfos :: forall a. (Ord a, Fixpoint a) => [Char] -> [SubC a] -> [Doc]
pprSinfos [Char]
msg = (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (([Char] -> Doc
text [Char]
msg Doc -> Doc -> Doc
<->) (Doc -> Doc) -> (a -> Doc) -> a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
forall a. Fixpoint a => a -> Doc
toFix) ([a] -> [Doc]) -> ([SubC a] -> [a]) -> [SubC a] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [a]
forall a. Ord a => [a] -> [a]
L.sort ([a] -> [a]) -> ([SubC a] -> [a]) -> [SubC a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SubC a -> a) -> [SubC a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SubC a -> a
forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo
instance Fixpoint a => Show (WfC a) where
show :: WfC a -> [Char]
show = WfC a -> [Char]
forall a. Fixpoint a => a -> [Char]
showFix
instance Fixpoint a => Show (SubC a) where
show :: SubC a -> [Char]
show = SubC a -> [Char]
forall a. Fixpoint a => a -> [Char]
showFix
instance Fixpoint a => Show (SimpC a) where
show :: SimpC a -> [Char]
show = SimpC a -> [Char]
forall a. Fixpoint a => a -> [Char]
showFix
instance Fixpoint a => PPrint (SubC a) where
pprintTidy :: Tidy -> SubC a -> Doc
pprintTidy Tidy
_ = SubC a -> Doc
forall a. Fixpoint a => a -> Doc
toFix
instance Fixpoint a => PPrint (SimpC a) where
pprintTidy :: Tidy -> SimpC a -> Doc
pprintTidy Tidy
_ = SimpC a -> Doc
forall a. Fixpoint a => a -> Doc
toFix
instance Fixpoint a => PPrint (WfC a) where
pprintTidy :: Tidy -> WfC a -> Doc
pprintTidy Tidy
_ = WfC a -> Doc
forall a. Fixpoint a => a -> Doc
toFix
instance Fixpoint a => Fixpoint (SubC a) where
toFix :: SubC a -> Doc
toFix SubC a
c = Doc -> Int -> Doc -> Doc
hang ([Char] -> Doc
text [Char]
"\n\nconstraint:") Int
2 Doc
bd
where bd :: Doc
bd = IBindEnv -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SubC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
c)
Doc -> Doc -> Doc
$+$ [Char] -> Doc
text [Char]
"lhs" Doc -> Doc -> Doc
<+> SortedReft -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
c)
Doc -> Doc -> Doc
$+$ [Char] -> Doc
text [Char]
"rhs" Doc -> Doc -> Doc
<+> SortedReft -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs SubC a
c)
Doc -> Doc -> Doc
$+$ (Maybe Integer -> Doc
forall a. Show a => Maybe a -> Doc
pprId (SubC a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
sid SubC a
c) Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"tag" Doc -> Doc -> Doc
<+> Tag -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SubC a -> Tag
forall (c :: * -> *) a. TaggedC c a => c a -> Tag
stag SubC a
c))
Doc -> Doc -> Doc
$+$ Doc -> Doc -> Doc
toFixMeta ([Char] -> Doc
text [Char]
"constraint" Doc -> Doc -> Doc
<+> Maybe Integer -> Doc
forall a. Show a => Maybe a -> Doc
pprId (SubC a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
sid SubC a
c)) (a -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SubC a -> a
forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SubC a
c))
instance Fixpoint a => Fixpoint (SimpC a) where
toFix :: SimpC a -> Doc
toFix SimpC a
c = Doc -> Int -> Doc -> Doc
hang ([Char] -> Doc
text [Char]
"\n\nsimpleConstraint:") Int
2 Doc
bd
where bd :: Doc
bd = IBindEnv -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC a
c)
Doc -> Doc -> Doc
$+$ [Char] -> Doc
text [Char]
"rhs" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SimpC a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
crhs SimpC a
c)
Doc -> Doc -> Doc
$+$ (Maybe Integer -> Doc
forall a. Show a => Maybe a -> Doc
pprId (SimpC a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
sid SimpC a
c) Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"tag" Doc -> Doc -> Doc
<+> Tag -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SimpC a -> Tag
forall (c :: * -> *) a. TaggedC c a => c a -> Tag
stag SimpC a
c))
Doc -> Doc -> Doc
$+$ Doc -> Doc -> Doc
toFixMeta ([Char] -> Doc
text [Char]
"simpleConstraint" Doc -> Doc -> Doc
<+> Maybe Integer -> Doc
forall a. Show a => Maybe a -> Doc
pprId (SimpC a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
sid SimpC a
c)) (a -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SimpC a -> a
forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SimpC a
c))
instance Fixpoint a => Fixpoint (WfC a) where
toFix :: WfC a -> Doc
toFix WfC a
w = Doc -> Int -> Doc -> Doc
hang ([Char] -> Doc
text [Char]
"\n\nwf:") Int
2 Doc
bd
where bd :: Doc
bd = IBindEnv -> Doc
forall a. Fixpoint a => a -> Doc
toFix (WfC a -> IBindEnv
forall a. WfC a -> IBindEnv
wenv WfC a
w)
Doc -> Doc -> Doc
$+$ [Char] -> Doc
text [Char]
"reft" Doc -> Doc -> Doc
<+> SortedReft -> Doc
forall a. Fixpoint a => a -> Doc
toFix (Sort -> Reft -> SortedReft
RR Sort
t ((Symbol, Expr) -> Reft
Reft (Symbol
v, KVar -> Subst -> Expr
PKVar KVar
k Subst
forall a. Monoid a => a
mempty)))
Doc -> Doc -> Doc
$+$ Doc -> Doc -> Doc
toFixMeta ([Char] -> Doc
text [Char]
"wf") (a -> Doc
forall a. Fixpoint a => a -> Doc
toFix (WfC a -> a
forall a. WfC a -> a
winfo WfC a
w))
Doc -> Doc -> Doc
$+$ if WfC a -> Bool
forall a. WfC a -> Bool
isGWfc WfC a
w then Doc -> Doc -> Doc
toFixMeta ([Char] -> Doc
text [Char]
"expr") (Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix (WfC a -> Expr
forall a. WfC a -> Expr
wexpr WfC a
w)) else Doc
forall a. Monoid a => a
mempty
(Symbol
v, Sort
t, KVar
k) = WfC a -> (Symbol, Sort, KVar)
forall a. WfC a -> (Symbol, Sort, KVar)
wrft WfC a
w
toFixMeta :: Doc -> Doc -> Doc
toFixMeta :: Doc -> Doc -> Doc
toFixMeta Doc
k Doc
v = [Char] -> Doc
text [Char]
"// META" Doc -> Doc -> Doc
<+> Doc
k Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
":" Doc -> Doc -> Doc
<+> Doc
v
pprId :: Show a => Maybe a -> Doc
pprId :: forall a. Show a => Maybe a -> Doc
pprId (Just a
i) = Doc
"id" Doc -> Doc -> Doc
<+> a -> Doc
forall a. Show a => a -> Doc
tshow a
i
pprId Maybe a
_ = Doc
""
instance PPrint GFixSolution where
pprintTidy :: Tidy -> GFixSolution -> Doc
pprintTidy Tidy
k (GSol HashMap KVar (Expr, [Expr])
xs) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
"\n\n" (Tidy -> (KVar, (Expr, [Expr])) -> Doc
pprintTidyGradual Tidy
k ((KVar, (Expr, [Expr])) -> Doc)
-> [(KVar, (Expr, [Expr]))] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap KVar (Expr, [Expr]) -> [(KVar, (Expr, [Expr]))]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap KVar (Expr, [Expr])
xs)
pprintTidyGradual :: Tidy -> (KVar, (Expr, [Expr])) -> Doc
pprintTidyGradual :: Tidy -> (KVar, (Expr, [Expr])) -> Doc
pprintTidyGradual Tidy
_ (KVar
x, (Expr
e, [Expr]
es)) = KVar -> Doc
ppLocOfKVar KVar
x Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
":=" Doc -> Doc -> Doc
<+> (Doc -> Expr -> Doc
ppNonTauto Doc
" && " Expr
e Doc -> Doc -> Doc
<-> [Expr] -> Doc
forall a. PPrint a => a -> Doc
pprint [Expr]
es)
ppLocOfKVar :: KVar -> Doc
ppLocOfKVar :: KVar -> Doc
ppLocOfKVar = [Char] -> Doc
text([Char] -> Doc) -> (KVar -> [Char]) -> KVar -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/=Char
'(') ([Char] -> [Char]) -> (KVar -> [Char]) -> KVar -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> [Char]
symbolString (Symbol -> [Char]) -> (KVar -> Symbol) -> KVar -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.KVar -> Symbol
kv
ppNonTauto :: Doc -> Expr -> Doc
ppNonTauto :: Doc -> Expr -> Doc
ppNonTauto Doc
d Expr
e
| Expr -> Bool
isTautoPred Expr
e = Doc
forall a. Monoid a => a
mempty
| Bool
otherwise = Expr -> Doc
forall a. PPrint a => a -> Doc
pprint Expr
e Doc -> Doc -> Doc
<-> Doc
d
instance Show GFixSolution where
show :: GFixSolution -> [Char]
show = GFixSolution -> [Char]
forall a. PPrint a => a -> [Char]
showpp
instance S.Store QualPattern
instance S.Store QualParam
instance S.Store Qualifier
instance S.Store Kuts
instance S.Store HOInfo
instance S.Store GWInfo
instance S.Store GFixSolution
instance (S.Store a) => S.Store (SubC a)
instance (S.Store a) => S.Store (WfC a)
instance (S.Store a) => S.Store (SimpC a)
instance (S.Store (c a), S.Store a) => S.Store (GInfo c a)
instance NFData QualPattern
instance NFData QualParam
instance NFData Qualifier
instance NFData Kuts
instance NFData HOInfo
instance NFData GFixSolution
instance NFData GWInfo
instance (NFData a) => NFData (SubC a)
instance (NFData a) => NFData (WfC a)
instance (NFData a) => NFData (SimpC a)
instance (NFData (c a), NFData a) => NFData (GInfo c a)
instance (NFData a) => NFData (Result a)
instance Hashable Qualifier
instance Hashable QualPattern
instance Hashable QualParam
instance Hashable Equation
instance B.Binary QualPattern
instance B.Binary QualParam
instance B.Binary Qualifier
wfC :: (Fixpoint a) => IBindEnv -> SortedReft -> a -> [WfC a]
wfC :: forall a. Fixpoint a => IBindEnv -> SortedReft -> a -> [WfC a]
wfC IBindEnv
be SortedReft
sr a
x = if (Subst -> Bool) -> [Subst] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Subst -> Bool
isEmptySubst [Subst]
sus
then [IBindEnv -> (Symbol, Sort, KVar) -> a -> WfC a
forall a. IBindEnv -> (Symbol, Sort, KVar) -> a -> WfC a
WfC IBindEnv
be (Symbol
v, SortedReft -> Sort
sr_sort SortedReft
sr, KVar
k) a
x | KVar
k <- [KVar]
ks ]
[WfC a] -> [WfC a] -> [WfC a]
forall a. [a] -> [a] -> [a]
++ [IBindEnv -> (Symbol, Sort, KVar) -> a -> Expr -> GradInfo -> WfC a
forall a.
IBindEnv -> (Symbol, Sort, KVar) -> a -> Expr -> GradInfo -> WfC a
GWfC IBindEnv
be (Symbol
v, SortedReft -> Sort
sr_sort SortedReft
sr, KVar
k) a
x Expr
e GradInfo
i | (KVar
k, Expr
e, GradInfo
i) <- [(KVar, Expr, GradInfo)]
gs ]
else [Char] -> [WfC a]
forall a. (?callStack::CallStack) => [Char] -> a
errorstar [Char]
msg
where
msg :: [Char]
msg = [Char]
"wfKvar: malformed wfC " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SortedReft -> [Char]
forall a. Show a => a -> [Char]
show SortedReft
sr [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Subst] -> [Char]
forall a. Show a => a -> [Char]
show ([Subst]
sus [Subst] -> [Subst] -> [Subst]
forall a. [a] -> [a] -> [a]
++ [Subst]
gsus)
Reft (Symbol
v, Expr
ras) = SortedReft -> Reft
sr_reft SortedReft
sr
([KVar]
ks, [Subst]
sus) = [(KVar, Subst)] -> ([KVar], [Subst])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(KVar, Subst)] -> ([KVar], [Subst]))
-> [(KVar, Subst)] -> ([KVar], [Subst])
forall a b. (a -> b) -> a -> b
$ Expr -> [(KVar, Subst)]
go Expr
ras
([(KVar, Expr, GradInfo)]
gs, [Subst]
gsus) = [((KVar, Expr, GradInfo), Subst)]
-> ([(KVar, Expr, GradInfo)], [Subst])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((KVar, Expr, GradInfo), Subst)]
-> ([(KVar, Expr, GradInfo)], [Subst]))
-> [((KVar, Expr, GradInfo), Subst)]
-> ([(KVar, Expr, GradInfo)], [Subst])
forall a b. (a -> b) -> a -> b
$ Expr -> [((KVar, Expr, GradInfo), Subst)]
go' Expr
ras
go :: Expr -> [(KVar, Subst)]
go (PKVar KVar
k Subst
su) = [(KVar
k, Subst
su)]
go (PAnd [Expr]
es) = [(KVar
k, Subst
su) | PKVar KVar
k Subst
su <- [Expr]
es]
go Expr
_ = []
go' :: Expr -> [((KVar, Expr, GradInfo), Subst)]
go' (PGrad KVar
k Subst
su GradInfo
i Expr
e) = [((KVar
k, Expr
e, GradInfo
i), Subst
su)]
go' (PAnd [Expr]
es) = (Expr -> [((KVar, Expr, GradInfo), Subst)])
-> [Expr] -> [((KVar, Expr, GradInfo), Subst)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [((KVar, Expr, GradInfo), Subst)]
go' [Expr]
es
go' Expr
_ = []
mkSubC :: IBindEnv -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a
mkSubC :: forall a.
IBindEnv
-> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a
mkSubC = IBindEnv
-> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a
forall a.
IBindEnv
-> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a
SubC
subC :: IBindEnv -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> [SubC a]
subC :: forall a.
IBindEnv
-> SortedReft
-> SortedReft
-> Maybe Integer
-> Tag
-> a
-> [SubC a]
subC IBindEnv
γ SortedReft
sr1 SortedReft
sr2 Maybe Integer
i Tag
y a
z = [IBindEnv
-> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a
forall a.
IBindEnv
-> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a
SubC IBindEnv
γ SortedReft
sr1' (Reft -> SortedReft
sr2' Reft
r2') Maybe Integer
i Tag
y a
z | Reft
r2' <- Reft -> [Reft]
reftConjuncts Reft
r2]
where
RR Sort
t1 Reft
r1 = SortedReft
sr1
RR Sort
t2 Reft
r2 = SortedReft
sr2
sr1' :: SortedReft
sr1' = Sort -> Reft -> SortedReft
RR Sort
t1 (Reft -> SortedReft) -> Reft -> SortedReft
forall a b. (a -> b) -> a -> b
$ Reft -> Symbol -> Reft
shiftVV Reft
r1 Symbol
vv'
sr2' :: Reft -> SortedReft
sr2' Reft
r2' = Sort -> Reft -> SortedReft
RR Sort
t2 (Reft -> SortedReft) -> Reft -> SortedReft
forall a b. (a -> b) -> a -> b
$ Reft -> Symbol -> Reft
shiftVV Reft
r2' Symbol
vv'
vv' :: Symbol
vv' = Maybe Integer -> Symbol
mkVV Maybe Integer
i
mkVV :: Maybe Integer -> Symbol
mkVV :: Maybe Integer -> Symbol
mkVV (Just Integer
i) = Maybe Integer -> Symbol
vv (Maybe Integer -> Symbol) -> Maybe Integer -> Symbol
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
mkVV Maybe Integer
Nothing = Symbol
vvCon
shiftVV :: Reft -> Symbol -> Reft
shiftVV :: Reft -> Symbol -> Reft
shiftVV r :: Reft
r@(Reft (Symbol
v, Expr
ras)) Symbol
v'
| Symbol
v Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
v' = Reft
r
| Bool
otherwise = (Symbol, Expr) -> Reft
Reft (Symbol
v', Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 Expr
ras (Symbol
v, Symbol -> Expr
EVar Symbol
v'))
addIds :: [SubC a] -> [(Integer, SubC a)]
addIds :: forall a. [SubC a] -> [(Integer, SubC a)]
addIds = (Integer -> SubC a -> (Integer, SubC a))
-> [Integer] -> [SubC a] -> [(Integer, SubC a)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Integer
i SubC a
c -> (Integer
i, Integer -> SubC a -> SubC a
forall {a} {a}. Show a => a -> SubC a -> SubC a
shiftId Integer
i (SubC a -> SubC a) -> SubC a -> SubC a
forall a b. (a -> b) -> a -> b
$ SubC a
c {_sid = Just i})) [Integer
1..]
where
shiftId :: a -> SubC a -> SubC a
shiftId a
i SubC a
c = SubC a
c { slhs = shiftSR i (slhs c) }
{ srhs = shiftSR i (srhs c) }
shiftSR :: a -> SortedReft -> SortedReft
shiftSR a
i SortedReft
sr = SortedReft
sr { sr_reft = shiftR i $ sr_reft sr }
shiftR :: a -> Reft -> Reft
shiftR a
i r :: Reft
r@(Reft (Symbol
v, Expr
_)) = Reft -> Symbol -> Reft
shiftVV Reft
r (Symbol -> a -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
v a
i)
data Qualifier = Q
{ Qualifier -> Symbol
qName :: !Symbol
, Qualifier -> [QualParam]
qParams :: [QualParam]
, Qualifier -> Expr
qBody :: !Expr
, Qualifier -> SourcePos
qPos :: !SourcePos
}
deriving (Qualifier -> Qualifier -> Bool
(Qualifier -> Qualifier -> Bool)
-> (Qualifier -> Qualifier -> Bool) -> Eq Qualifier
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Qualifier -> Qualifier -> Bool
== :: Qualifier -> Qualifier -> Bool
$c/= :: Qualifier -> Qualifier -> Bool
/= :: Qualifier -> Qualifier -> Bool
Eq, Eq Qualifier
Eq Qualifier =>
(Qualifier -> Qualifier -> Ordering)
-> (Qualifier -> Qualifier -> Bool)
-> (Qualifier -> Qualifier -> Bool)
-> (Qualifier -> Qualifier -> Bool)
-> (Qualifier -> Qualifier -> Bool)
-> (Qualifier -> Qualifier -> Qualifier)
-> (Qualifier -> Qualifier -> Qualifier)
-> Ord Qualifier
Qualifier -> Qualifier -> Bool
Qualifier -> Qualifier -> Ordering
Qualifier -> Qualifier -> Qualifier
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Qualifier -> Qualifier -> Ordering
compare :: Qualifier -> Qualifier -> Ordering
$c< :: Qualifier -> Qualifier -> Bool
< :: Qualifier -> Qualifier -> Bool
$c<= :: Qualifier -> Qualifier -> Bool
<= :: Qualifier -> Qualifier -> Bool
$c> :: Qualifier -> Qualifier -> Bool
> :: Qualifier -> Qualifier -> Bool
$c>= :: Qualifier -> Qualifier -> Bool
>= :: Qualifier -> Qualifier -> Bool
$cmax :: Qualifier -> Qualifier -> Qualifier
max :: Qualifier -> Qualifier -> Qualifier
$cmin :: Qualifier -> Qualifier -> Qualifier
min :: Qualifier -> Qualifier -> Qualifier
Ord, Int -> Qualifier -> [Char] -> [Char]
[Qualifier] -> [Char] -> [Char]
Qualifier -> [Char]
(Int -> Qualifier -> [Char] -> [Char])
-> (Qualifier -> [Char])
-> ([Qualifier] -> [Char] -> [Char])
-> Show Qualifier
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> Qualifier -> [Char] -> [Char]
showsPrec :: Int -> Qualifier -> [Char] -> [Char]
$cshow :: Qualifier -> [Char]
show :: Qualifier -> [Char]
$cshowList :: [Qualifier] -> [Char] -> [Char]
showList :: [Qualifier] -> [Char] -> [Char]
Show, Typeable Qualifier
Typeable Qualifier =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Qualifier -> c Qualifier)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Qualifier)
-> (Qualifier -> Constr)
-> (Qualifier -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Qualifier))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Qualifier))
-> ((forall b. Data b => b -> b) -> Qualifier -> Qualifier)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r)
-> (forall u. (forall d. Data d => d -> u) -> Qualifier -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> Qualifier -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier)
-> Data Qualifier
Qualifier -> Constr
Qualifier -> DataType
(forall b. Data b => b -> b) -> Qualifier -> Qualifier
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Qualifier -> u
forall u. (forall d. Data d => d -> u) -> Qualifier -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Qualifier
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Qualifier -> c Qualifier
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Qualifier)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Qualifier)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Qualifier -> c Qualifier
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Qualifier -> c Qualifier
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Qualifier
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Qualifier
$ctoConstr :: Qualifier -> Constr
toConstr :: Qualifier -> Constr
$cdataTypeOf :: Qualifier -> DataType
dataTypeOf :: Qualifier -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Qualifier)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Qualifier)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Qualifier)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Qualifier)
$cgmapT :: (forall b. Data b => b -> b) -> Qualifier -> Qualifier
gmapT :: (forall b. Data b => b -> b) -> Qualifier -> Qualifier
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Qualifier -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Qualifier -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Qualifier -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Qualifier -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Qualifier -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Qualifier -> m Qualifier
Data, Typeable, (forall x. Qualifier -> Rep Qualifier x)
-> (forall x. Rep Qualifier x -> Qualifier) -> Generic Qualifier
forall x. Rep Qualifier x -> Qualifier
forall x. Qualifier -> Rep Qualifier x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Qualifier -> Rep Qualifier x
from :: forall x. Qualifier -> Rep Qualifier x
$cto :: forall x. Rep Qualifier x -> Qualifier
to :: forall x. Rep Qualifier x -> Qualifier
Generic)
data QualParam = QP
{ QualParam -> Symbol
qpSym :: !Symbol
, QualParam -> QualPattern
qpPat :: !QualPattern
, QualParam -> Sort
qpSort :: !Sort
}
deriving (QualParam -> QualParam -> Bool
(QualParam -> QualParam -> Bool)
-> (QualParam -> QualParam -> Bool) -> Eq QualParam
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: QualParam -> QualParam -> Bool
== :: QualParam -> QualParam -> Bool
$c/= :: QualParam -> QualParam -> Bool
/= :: QualParam -> QualParam -> Bool
Eq, Eq QualParam
Eq QualParam =>
(QualParam -> QualParam -> Ordering)
-> (QualParam -> QualParam -> Bool)
-> (QualParam -> QualParam -> Bool)
-> (QualParam -> QualParam -> Bool)
-> (QualParam -> QualParam -> Bool)
-> (QualParam -> QualParam -> QualParam)
-> (QualParam -> QualParam -> QualParam)
-> Ord QualParam
QualParam -> QualParam -> Bool
QualParam -> QualParam -> Ordering
QualParam -> QualParam -> QualParam
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: QualParam -> QualParam -> Ordering
compare :: QualParam -> QualParam -> Ordering
$c< :: QualParam -> QualParam -> Bool
< :: QualParam -> QualParam -> Bool
$c<= :: QualParam -> QualParam -> Bool
<= :: QualParam -> QualParam -> Bool
$c> :: QualParam -> QualParam -> Bool
> :: QualParam -> QualParam -> Bool
$c>= :: QualParam -> QualParam -> Bool
>= :: QualParam -> QualParam -> Bool
$cmax :: QualParam -> QualParam -> QualParam
max :: QualParam -> QualParam -> QualParam
$cmin :: QualParam -> QualParam -> QualParam
min :: QualParam -> QualParam -> QualParam
Ord, Int -> QualParam -> [Char] -> [Char]
[QualParam] -> [Char] -> [Char]
QualParam -> [Char]
(Int -> QualParam -> [Char] -> [Char])
-> (QualParam -> [Char])
-> ([QualParam] -> [Char] -> [Char])
-> Show QualParam
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> QualParam -> [Char] -> [Char]
showsPrec :: Int -> QualParam -> [Char] -> [Char]
$cshow :: QualParam -> [Char]
show :: QualParam -> [Char]
$cshowList :: [QualParam] -> [Char] -> [Char]
showList :: [QualParam] -> [Char] -> [Char]
Show, Typeable QualParam
Typeable QualParam =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualParam -> c QualParam)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QualParam)
-> (QualParam -> Constr)
-> (QualParam -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QualParam))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QualParam))
-> ((forall b. Data b => b -> b) -> QualParam -> QualParam)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualParam -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualParam -> r)
-> (forall u. (forall d. Data d => d -> u) -> QualParam -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> QualParam -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam)
-> Data QualParam
QualParam -> Constr
QualParam -> DataType
(forall b. Data b => b -> b) -> QualParam -> QualParam
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> QualParam -> u
forall u. (forall d. Data d => d -> u) -> QualParam -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualParam -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualParam -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QualParam
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualParam -> c QualParam
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QualParam)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QualParam)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualParam -> c QualParam
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualParam -> c QualParam
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QualParam
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QualParam
$ctoConstr :: QualParam -> Constr
toConstr :: QualParam -> Constr
$cdataTypeOf :: QualParam -> DataType
dataTypeOf :: QualParam -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QualParam)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QualParam)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QualParam)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QualParam)
$cgmapT :: (forall b. Data b => b -> b) -> QualParam -> QualParam
gmapT :: (forall b. Data b => b -> b) -> QualParam -> QualParam
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualParam -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualParam -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualParam -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualParam -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> QualParam -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> QualParam -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QualParam -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QualParam -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualParam -> m QualParam
Data, Typeable, (forall x. QualParam -> Rep QualParam x)
-> (forall x. Rep QualParam x -> QualParam) -> Generic QualParam
forall x. Rep QualParam x -> QualParam
forall x. QualParam -> Rep QualParam x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. QualParam -> Rep QualParam x
from :: forall x. QualParam -> Rep QualParam x
$cto :: forall x. Rep QualParam x -> QualParam
to :: forall x. Rep QualParam x -> QualParam
Generic)
data QualPattern
= PatNone
| PatPrefix !Symbol !Int
| PatSuffix !Int !Symbol
| PatExact !Symbol
deriving (QualPattern -> QualPattern -> Bool
(QualPattern -> QualPattern -> Bool)
-> (QualPattern -> QualPattern -> Bool) -> Eq QualPattern
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: QualPattern -> QualPattern -> Bool
== :: QualPattern -> QualPattern -> Bool
$c/= :: QualPattern -> QualPattern -> Bool
/= :: QualPattern -> QualPattern -> Bool
Eq, Eq QualPattern
Eq QualPattern =>
(QualPattern -> QualPattern -> Ordering)
-> (QualPattern -> QualPattern -> Bool)
-> (QualPattern -> QualPattern -> Bool)
-> (QualPattern -> QualPattern -> Bool)
-> (QualPattern -> QualPattern -> Bool)
-> (QualPattern -> QualPattern -> QualPattern)
-> (QualPattern -> QualPattern -> QualPattern)
-> Ord QualPattern
QualPattern -> QualPattern -> Bool
QualPattern -> QualPattern -> Ordering
QualPattern -> QualPattern -> QualPattern
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: QualPattern -> QualPattern -> Ordering
compare :: QualPattern -> QualPattern -> Ordering
$c< :: QualPattern -> QualPattern -> Bool
< :: QualPattern -> QualPattern -> Bool
$c<= :: QualPattern -> QualPattern -> Bool
<= :: QualPattern -> QualPattern -> Bool
$c> :: QualPattern -> QualPattern -> Bool
> :: QualPattern -> QualPattern -> Bool
$c>= :: QualPattern -> QualPattern -> Bool
>= :: QualPattern -> QualPattern -> Bool
$cmax :: QualPattern -> QualPattern -> QualPattern
max :: QualPattern -> QualPattern -> QualPattern
$cmin :: QualPattern -> QualPattern -> QualPattern
min :: QualPattern -> QualPattern -> QualPattern
Ord, Int -> QualPattern -> [Char] -> [Char]
[QualPattern] -> [Char] -> [Char]
QualPattern -> [Char]
(Int -> QualPattern -> [Char] -> [Char])
-> (QualPattern -> [Char])
-> ([QualPattern] -> [Char] -> [Char])
-> Show QualPattern
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> QualPattern -> [Char] -> [Char]
showsPrec :: Int -> QualPattern -> [Char] -> [Char]
$cshow :: QualPattern -> [Char]
show :: QualPattern -> [Char]
$cshowList :: [QualPattern] -> [Char] -> [Char]
showList :: [QualPattern] -> [Char] -> [Char]
Show, Typeable QualPattern
Typeable QualPattern =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualPattern -> c QualPattern)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QualPattern)
-> (QualPattern -> Constr)
-> (QualPattern -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QualPattern))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c QualPattern))
-> ((forall b. Data b => b -> b) -> QualPattern -> QualPattern)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualPattern -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualPattern -> r)
-> (forall u. (forall d. Data d => d -> u) -> QualPattern -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> QualPattern -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern)
-> Data QualPattern
QualPattern -> Constr
QualPattern -> DataType
(forall b. Data b => b -> b) -> QualPattern -> QualPattern
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> QualPattern -> u
forall u. (forall d. Data d => d -> u) -> QualPattern -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualPattern -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualPattern -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QualPattern
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualPattern -> c QualPattern
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QualPattern)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c QualPattern)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualPattern -> c QualPattern
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QualPattern -> c QualPattern
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QualPattern
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QualPattern
$ctoConstr :: QualPattern -> Constr
toConstr :: QualPattern -> Constr
$cdataTypeOf :: QualPattern -> DataType
dataTypeOf :: QualPattern -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QualPattern)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QualPattern)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c QualPattern)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c QualPattern)
$cgmapT :: (forall b. Data b => b -> b) -> QualPattern -> QualPattern
gmapT :: (forall b. Data b => b -> b) -> QualPattern -> QualPattern
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualPattern -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QualPattern -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualPattern -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QualPattern -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> QualPattern -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> QualPattern -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QualPattern -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QualPattern -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QualPattern -> m QualPattern
Data, Typeable, (forall x. QualPattern -> Rep QualPattern x)
-> (forall x. Rep QualPattern x -> QualPattern)
-> Generic QualPattern
forall x. Rep QualPattern x -> QualPattern
forall x. QualPattern -> Rep QualPattern x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. QualPattern -> Rep QualPattern x
from :: forall x. QualPattern -> Rep QualPattern x
$cto :: forall x. Rep QualPattern x -> QualPattern
to :: forall x. Rep QualPattern x -> QualPattern
Generic)
trueQual :: Qualifier
trueQual :: Qualifier
trueQual = Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
Q ([Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol ([Char]
"QTrue" :: String)) [] Expr
forall a. Monoid a => a
mempty ([Char] -> SourcePos
dummyPos [Char]
"trueQual")
instance Loc Qualifier where
srcSpan :: Qualifier -> SrcSpan
srcSpan Qualifier
q = SourcePos -> SourcePos -> SrcSpan
SS SourcePos
l SourcePos
l
where
l :: SourcePos
l = Qualifier -> SourcePos
qPos Qualifier
q
instance Subable Qualifier where
syms :: Qualifier -> [Symbol]
syms = Qualifier -> [Symbol]
qualFreeSymbols
subst :: Subst -> Qualifier -> Qualifier
subst = (Expr -> Expr) -> Qualifier -> Qualifier
mapQualBody ((Expr -> Expr) -> Qualifier -> Qualifier)
-> (Subst -> Expr -> Expr) -> Subst -> Qualifier -> Qualifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
subst
substf :: (Symbol -> Expr) -> Qualifier -> Qualifier
substf = (Expr -> Expr) -> Qualifier -> Qualifier
mapQualBody ((Expr -> Expr) -> Qualifier -> Qualifier)
-> ((Symbol -> Expr) -> Expr -> Expr)
-> (Symbol -> Expr)
-> Qualifier
-> Qualifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Expr) -> Expr -> Expr
forall a. Subable a => (Symbol -> Expr) -> a -> a
substf
substa :: (Symbol -> Symbol) -> Qualifier -> Qualifier
substa = (Expr -> Expr) -> Qualifier -> Qualifier
mapQualBody ((Expr -> Expr) -> Qualifier -> Qualifier)
-> ((Symbol -> Symbol) -> Expr -> Expr)
-> (Symbol -> Symbol)
-> Qualifier
-> Qualifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Symbol) -> Expr -> Expr
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa
mapQualBody :: (Expr -> Expr) -> Qualifier -> Qualifier
mapQualBody :: (Expr -> Expr) -> Qualifier -> Qualifier
mapQualBody Expr -> Expr
f Qualifier
q = Qualifier
q { qBody = f (qBody q) }
qualFreeSymbols :: Qualifier -> [Symbol]
qualFreeSymbols :: Qualifier -> [Symbol]
qualFreeSymbols Qualifier
q = (Symbol -> Bool) -> [Symbol] -> [Symbol]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Symbol -> Bool) -> Symbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Bool
isPrim) [Symbol]
xs
where
xs :: [Symbol]
xs = Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms (Qualifier -> Expr
qBody Qualifier
q) [Symbol] -> [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a] -> [a]
L.\\ [Symbol] -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms (QualParam -> Symbol
qpSym (QualParam -> Symbol) -> [QualParam] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Qualifier -> [QualParam]
qParams Qualifier
q)
instance Fixpoint QualParam where
toFix :: QualParam -> Doc
toFix (QP Symbol
x QualPattern
_ Sort
t) = (Symbol, Sort) -> Doc
forall a. Fixpoint a => a -> Doc
toFix (Symbol
x, Sort
t)
instance PPrint QualParam where
pprintTidy :: Tidy -> QualParam -> Doc
pprintTidy Tidy
k (QP Symbol
x QualPattern
pat Sort
t) = Tidy -> Symbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
x Doc -> Doc -> Doc
<+> Tidy -> QualPattern -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k QualPattern
pat Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> Tidy -> Sort -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Sort
t
instance PPrint QualPattern where
pprintTidy :: Tidy -> QualPattern -> Doc
pprintTidy Tidy
_ QualPattern
PatNone = Doc
""
pprintTidy Tidy
k (PatPrefix Symbol
s Int
i) = Doc
"as" Doc -> Doc -> Doc
<+> Tidy -> Symbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
s Doc -> Doc -> Doc
<+> (Doc
"$" Doc -> Doc -> Doc
<-> Int -> Doc
forall a. PPrint a => a -> Doc
pprint Int
i)
pprintTidy Tidy
k (PatSuffix Int
s Symbol
i) = Doc
"as" Doc -> Doc -> Doc
<+> (Doc
"$" Doc -> Doc -> Doc
<-> Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
i) Doc -> Doc -> Doc
<+> Tidy -> Int -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Int
s
pprintTidy Tidy
k (PatExact Symbol
s ) = Doc
"~" Doc -> Doc -> Doc
<+> Tidy -> Symbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
s
instance Fixpoint Qualifier where
toFix :: Qualifier -> Doc
toFix = Qualifier -> Doc
pprQual
instance PPrint Qualifier where
pprintTidy :: Tidy -> Qualifier -> Doc
pprintTidy Tidy
k Qualifier
q = Doc
"qualif" Doc -> Doc -> Doc
<+> Tidy -> Symbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Qualifier -> Symbol
qName Qualifier
q) Doc -> Doc -> Doc
<+> Doc
"defined at" Doc -> Doc -> Doc
<+> Tidy -> SourcePos -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Qualifier -> SourcePos
qPos Qualifier
q)
pprQual :: Qualifier -> Doc
pprQual :: Qualifier -> Doc
pprQual (Q Symbol
n [QualParam]
xts Expr
p SourcePos
l) = [Char] -> Doc
text [Char]
"qualif" Doc -> Doc -> Doc
<+> [Char] -> Doc
text (Symbol -> [Char]
symbolString Symbol
n) Doc -> Doc -> Doc
<-> Doc -> Doc
parens Doc
args Doc -> Doc -> Doc
<-> Doc
colon Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix Expr
p) Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"//" Doc -> Doc -> Doc
<+> SourcePos -> Doc
forall a. Fixpoint a => a -> Doc
toFix SourcePos
l
where
args :: Doc
args = Doc -> [Doc] -> Doc
intersperse Doc
comma (QualParam -> Doc
forall a. Fixpoint a => a -> Doc
toFix (QualParam -> Doc) -> [QualParam] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [QualParam]
xts)
qualifier :: SEnv Sort -> SourcePos -> SEnv Sort -> Symbol -> Sort -> Expr -> Qualifier
qualifier :: SEnv Sort
-> SourcePos -> SEnv Sort -> Symbol -> Sort -> Expr -> Qualifier
qualifier SEnv Sort
lEnv SourcePos
l SEnv Sort
γ Symbol
v Sort
so Expr
p = Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier
mkQ Symbol
"Auto" ((Symbol
v, Sort
so) (Symbol, Sort) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. a -> [a] -> [a]
: [(Symbol, Sort)]
xts) Expr
p SourcePos
l
where
xs :: [Symbol]
xs = Symbol -> [Symbol] -> [Symbol]
forall a. Eq a => a -> [a] -> [a]
L.delete Symbol
v ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a]
L.nub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms Expr
p
xts :: [(Symbol, Sort)]
xts = [Maybe (Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Symbol, Sort)] -> [(Symbol, Sort)])
-> [Maybe (Symbol, Sort)] -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ (Symbol -> Integer -> Maybe (Symbol, Sort))
-> [Symbol] -> [Integer] -> [Maybe (Symbol, Sort)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (SourcePos
-> SEnv Sort
-> SEnv Sort
-> Symbol
-> Integer
-> Maybe (Symbol, Sort)
envSort SourcePos
l SEnv Sort
lEnv SEnv Sort
γ) [Symbol]
xs [Integer
0..]
mkQ :: Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier
mkQ :: Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier
mkQ Symbol
n = Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
Q Symbol
n ([QualParam] -> Expr -> SourcePos -> Qualifier)
-> ([(Symbol, Sort)] -> [QualParam])
-> [(Symbol, Sort)]
-> Expr
-> SourcePos
-> Qualifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, Sort)] -> [QualParam]
qualParams
qualParams :: [(Symbol, Sort)] -> [QualParam]
qualParams :: [(Symbol, Sort)] -> [QualParam]
qualParams [(Symbol, Sort)]
xts = [ Symbol -> QualPattern -> Sort -> QualParam
QP Symbol
x QualPattern
PatNone Sort
t | (Symbol
x, Sort
t) <- [(Symbol, Sort)]
xts]
qualBinds :: Qualifier -> [(Symbol, Sort)]
qualBinds :: Qualifier -> [(Symbol, Sort)]
qualBinds Qualifier
q = [ (QualParam -> Symbol
qpSym QualParam
qp, QualParam -> Sort
qpSort QualParam
qp) | QualParam
qp <- Qualifier -> [QualParam]
qParams Qualifier
q ]
envSort :: SourcePos -> SEnv Sort -> SEnv Sort -> Symbol -> Integer -> Maybe (Symbol, Sort)
envSort :: SourcePos
-> SEnv Sort
-> SEnv Sort
-> Symbol
-> Integer
-> Maybe (Symbol, Sort)
envSort SourcePos
l SEnv Sort
lEnv SEnv Sort
tEnv Symbol
x Integer
i
| Just Sort
t <- Symbol -> SEnv Sort -> Maybe Sort
forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
x SEnv Sort
tEnv = (Symbol, Sort) -> Maybe (Symbol, Sort)
forall a. a -> Maybe a
Just (Symbol
x, Sort
t)
| Just Sort
_ <- Symbol -> SEnv Sort -> Maybe Sort
forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
x SEnv Sort
lEnv = Maybe (Symbol, Sort)
forall a. Maybe a
Nothing
| Bool
otherwise = (Symbol, Sort) -> Maybe (Symbol, Sort)
forall a. a -> Maybe a
Just (Symbol
x, Sort
ai)
where
ai :: Sort
ai = LocSymbol -> Sort
fObj (LocSymbol -> Sort) -> LocSymbol -> Sort
forall a b. (a -> b) -> a -> b
$ SourcePos -> SourcePos -> Symbol -> LocSymbol
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l (Symbol -> LocSymbol) -> Symbol -> LocSymbol
forall a b. (a -> b) -> a -> b
$ Symbol -> Integer -> Symbol
tempSymbol Symbol
"LHTV" Integer
i
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)
mkQual :: Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
mkQual :: Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
mkQual Symbol
n [QualParam]
qps Expr
p = Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
Q Symbol
n [QualParam]
qps' Expr
p
where
qps' :: [QualParam]
qps' = (QualParam -> Sort -> QualParam)
-> [QualParam] -> [Sort] -> [QualParam]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\QualParam
qp Sort
t' -> QualParam
qp { qpSort = t'}) [QualParam]
qps [Sort]
ts'
ts' :: [Sort]
ts' = [Sort] -> [Sort]
gSorts (QualParam -> Sort
qpSort (QualParam -> Sort) -> [QualParam] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [QualParam]
qps)
gSorts :: [Sort] -> [Sort]
gSorts :: [Sort] -> [Sort]
gSorts [Sort]
ts = [(Symbol, Int)] -> Sort -> Sort
substVars [(Symbol, Int)]
su (Sort -> Sort) -> [Sort] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
ts
where
su :: [(Symbol, Int)]
su = ([Symbol] -> Tag -> [(Symbol, Int)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Int
0..]) ([Symbol] -> [(Symbol, Int)])
-> ([Sort] -> [Symbol]) -> [Sort] -> [(Symbol, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol] -> [Symbol]
forall a. Ord a => [a] -> [a]
sortNub ([Symbol] -> [Symbol])
-> ([Sort] -> [Symbol]) -> [Sort] -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort -> [Symbol]) -> [Sort] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Sort -> [Symbol]
sortVars ([Sort] -> [(Symbol, Int)]) -> [Sort] -> [(Symbol, Int)]
forall a b. (a -> b) -> a -> b
$ [Sort]
ts
substVars :: [(Symbol, Int)] -> Sort -> Sort
substVars :: [(Symbol, Int)] -> Sort -> Sort
substVars [(Symbol, Int)]
su = (Sort -> Sort) -> Sort -> Sort
mapSort' Sort -> Sort
tx
where
tx :: Sort -> Sort
tx (FObj Symbol
x)
| Just Int
i <- Symbol -> [(Symbol, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Symbol
x [(Symbol, Int)]
su = Int -> Sort
FVar Int
i
tx Sort
t = Sort
t
sortVars :: Sort -> [Symbol]
sortVars :: Sort -> [Symbol]
sortVars = ([Symbol] -> Sort -> [Symbol]) -> [Symbol] -> Sort -> [Symbol]
forall a. (a -> Sort -> a) -> a -> Sort -> a
foldSort' [Symbol] -> Sort -> [Symbol]
go []
where
go :: [Symbol] -> Sort -> [Symbol]
go [Symbol]
b (FObj Symbol
x) = Symbol
x Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
b
go [Symbol]
b Sort
_ = [Symbol]
b
mapSort' :: (Sort -> Sort) -> Sort -> Sort
mapSort' :: (Sort -> Sort) -> Sort -> Sort
mapSort' Sort -> Sort
f = Sort -> Sort
step
where
step :: Sort -> Sort
step = Sort -> Sort
go (Sort -> Sort) -> (Sort -> Sort) -> Sort -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Sort
f
go :: Sort -> Sort
go (FFunc Sort
t1 Sort
t2) = Sort -> Sort -> Sort
FFunc (Sort -> Sort
step Sort
t1) (Sort -> Sort
step Sort
t2)
go (FApp Sort
t1 Sort
t2) = Sort -> Sort -> Sort
FApp (Sort -> Sort
step Sort
t1) (Sort -> Sort
step Sort
t2)
go (FAbs Int
i Sort
t) = Int -> Sort -> Sort
FAbs Int
i (Sort -> Sort
step Sort
t)
go Sort
t = Sort
t
foldSort' :: (a -> Sort -> a) -> a -> Sort -> a
foldSort' :: forall a. (a -> Sort -> a) -> a -> Sort -> a
foldSort' a -> Sort -> a
f = a -> Sort -> a
step
where
step :: a -> Sort -> a
step a
b Sort
t = a -> Sort -> a
go (a -> Sort -> a
f a
b Sort
t) Sort
t
go :: a -> Sort -> a
go a
b (FFunc Sort
t1 Sort
t2) = (a -> Sort -> a) -> a -> [Sort] -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' a -> Sort -> a
step a
b [Sort
t1, Sort
t2]
go a
b (FApp Sort
t1 Sort
t2) = (a -> Sort -> a) -> a -> [Sort] -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' a -> Sort -> a
step a
b [Sort
t1, Sort
t2]
go a
b (FAbs Int
_ Sort
t) = a -> Sort -> a
go a
b Sort
t
go a
b Sort
_ = a
b
newtype Kuts = KS { Kuts -> HashSet KVar
ksVars :: S.HashSet KVar }
deriving (Kuts -> Kuts -> Bool
(Kuts -> Kuts -> Bool) -> (Kuts -> Kuts -> Bool) -> Eq Kuts
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Kuts -> Kuts -> Bool
== :: Kuts -> Kuts -> Bool
$c/= :: Kuts -> Kuts -> Bool
/= :: Kuts -> Kuts -> Bool
Eq, Int -> Kuts -> [Char] -> [Char]
[Kuts] -> [Char] -> [Char]
Kuts -> [Char]
(Int -> Kuts -> [Char] -> [Char])
-> (Kuts -> [Char]) -> ([Kuts] -> [Char] -> [Char]) -> Show Kuts
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> Kuts -> [Char] -> [Char]
showsPrec :: Int -> Kuts -> [Char] -> [Char]
$cshow :: Kuts -> [Char]
show :: Kuts -> [Char]
$cshowList :: [Kuts] -> [Char] -> [Char]
showList :: [Kuts] -> [Char] -> [Char]
Show, (forall x. Kuts -> Rep Kuts x)
-> (forall x. Rep Kuts x -> Kuts) -> Generic Kuts
forall x. Rep Kuts x -> Kuts
forall x. Kuts -> Rep Kuts x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Kuts -> Rep Kuts x
from :: forall x. Kuts -> Rep Kuts x
$cto :: forall x. Rep Kuts x -> Kuts
to :: forall x. Rep Kuts x -> Kuts
Generic)
instance Fixpoint Kuts where
toFix :: Kuts -> Doc
toFix (KS HashSet KVar
s) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Doc
"cut " Doc -> Doc -> Doc
<->) (Doc -> Doc) -> (KVar -> Doc) -> KVar -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KVar -> Doc
forall a. Fixpoint a => a -> Doc
toFix (KVar -> Doc) -> [KVar] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [KVar] -> [KVar]
forall a. Ord a => [a] -> [a]
L.sort (HashSet KVar -> [KVar]
forall a. HashSet a -> [a]
S.toList HashSet KVar
s)
ksMember :: KVar -> Kuts -> Bool
ksMember :: KVar -> Kuts -> Bool
ksMember KVar
k (KS HashSet KVar
s) = KVar -> HashSet KVar -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member KVar
k HashSet KVar
s
instance Semigroup Kuts where
Kuts
k1 <> :: Kuts -> Kuts -> Kuts
<> Kuts
k2 = HashSet KVar -> Kuts
KS (HashSet KVar -> Kuts) -> HashSet KVar -> Kuts
forall a b. (a -> b) -> a -> b
$ HashSet KVar -> HashSet KVar -> HashSet KVar
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Kuts -> HashSet KVar
ksVars Kuts
k1) (Kuts -> HashSet KVar
ksVars Kuts
k2)
instance Monoid Kuts where
mempty :: Kuts
mempty = HashSet KVar -> Kuts
KS HashSet KVar
forall a. HashSet a
S.empty
mappend :: Kuts -> Kuts -> Kuts
mappend = Kuts -> Kuts -> Kuts
forall a. Semigroup a => a -> a -> a
(<>)
fi :: [SubC a]
-> [WfC a]
-> BindEnv a
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> M.HashMap BindId a
-> Bool
-> Bool
-> [Triggered Expr]
-> AxiomEnv
-> [DataDecl]
-> [BindId]
-> GInfo SubC a
fi :: forall a.
[SubC a]
-> [WfC a]
-> BindEnv a
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap Int a
-> Bool
-> Bool
-> [Triggered Expr]
-> AxiomEnv
-> [DataDecl]
-> Tag
-> GInfo SubC a
fi [SubC a]
cs [WfC a]
ws BindEnv a
binds SEnv Sort
ls SEnv Sort
ds Kuts
ks [Qualifier]
qs HashMap Int a
bi Bool
aHO Bool
aHOq [Triggered Expr]
es AxiomEnv
axe [DataDecl]
adts Tag
ebs
= FI { cm :: HashMap Integer (SubC a)
cm = [(Integer, SubC a)] -> HashMap Integer (SubC a)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Integer, SubC a)] -> HashMap Integer (SubC a))
-> [(Integer, SubC a)] -> HashMap Integer (SubC a)
forall a b. (a -> b) -> a -> b
$ [SubC a] -> [(Integer, SubC a)]
forall a. [SubC a] -> [(Integer, SubC a)]
addIds [SubC a]
cs
, ws :: HashMap KVar (WfC a)
ws = (WfC a -> WfC a -> WfC a)
-> [(KVar, WfC a)] -> HashMap KVar (WfC a)
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> [(k, v)] -> HashMap k v
M.fromListWith WfC a -> WfC a -> WfC a
forall {a}. a
err [(KVar
k, WfC a
w) | WfC a
w <- [WfC a]
ws, let (Symbol
_, Sort
_, KVar
k) = WfC a -> (Symbol, Sort, KVar)
forall a. WfC a -> (Symbol, Sort, KVar)
wrft WfC a
w]
, bs :: BindEnv a
bs = (Int -> BindEnv a -> BindEnv a) -> BindEnv a -> Tag -> BindEnv a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (((Symbol, SortedReft) -> (Symbol, SortedReft))
-> Int -> BindEnv a -> BindEnv a
forall a.
((Symbol, SortedReft) -> (Symbol, SortedReft))
-> Int -> BindEnv a -> BindEnv a
adjustBindEnv (Symbol, SortedReft) -> (Symbol, SortedReft)
forall {a}. (a, SortedReft) -> (a, SortedReft)
stripReft) BindEnv a
binds Tag
ebs
, gLits :: SEnv Sort
gLits = SEnv Sort
ls
, dLits :: SEnv Sort
dLits = SEnv Sort
ds
, kuts :: Kuts
kuts = Kuts
ks
, quals :: [Qualifier]
quals = [Qualifier]
qs
, bindInfo :: HashMap Int a
bindInfo = HashMap Int a
bi
, hoInfo :: HOInfo
hoInfo = Bool -> Bool -> HOInfo
HOI Bool
aHO Bool
aHOq
, asserts :: [Triggered Expr]
asserts = [Triggered Expr]
es
, ae :: AxiomEnv
ae = AxiomEnv
axe
, ddecls :: [DataDecl]
ddecls = [DataDecl]
adts
, ebinds :: Tag
ebinds = Tag
ebs
}
where
err :: a
err = [Char] -> a
forall a. (?callStack::CallStack) => [Char] -> a
errorstar [Char]
"multiple WfCs with same kvar"
stripReft :: (a, SortedReft) -> (a, SortedReft)
stripReft (a
sym, SortedReft
reft) = (a
sym, SortedReft
reft { sr_reft = trueReft })
data FInfoWithOpts a = FIO
{ forall a. FInfoWithOpts a -> FInfo a
fioFI :: FInfo a
, forall a. FInfoWithOpts a -> [[Char]]
fioOpts :: [String]
}
type FInfo a = GInfo SubC a
type SInfo a = GInfo SimpC a
data HOInfo = HOI
{ HOInfo -> Bool
hoBinds :: Bool
, HOInfo -> Bool
hoQuals :: Bool
}
deriving (HOInfo -> HOInfo -> Bool
(HOInfo -> HOInfo -> Bool)
-> (HOInfo -> HOInfo -> Bool) -> Eq HOInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HOInfo -> HOInfo -> Bool
== :: HOInfo -> HOInfo -> Bool
$c/= :: HOInfo -> HOInfo -> Bool
/= :: HOInfo -> HOInfo -> Bool
Eq, Int -> HOInfo -> [Char] -> [Char]
[HOInfo] -> [Char] -> [Char]
HOInfo -> [Char]
(Int -> HOInfo -> [Char] -> [Char])
-> (HOInfo -> [Char])
-> ([HOInfo] -> [Char] -> [Char])
-> Show HOInfo
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> HOInfo -> [Char] -> [Char]
showsPrec :: Int -> HOInfo -> [Char] -> [Char]
$cshow :: HOInfo -> [Char]
show :: HOInfo -> [Char]
$cshowList :: [HOInfo] -> [Char] -> [Char]
showList :: [HOInfo] -> [Char] -> [Char]
Show, (forall x. HOInfo -> Rep HOInfo x)
-> (forall x. Rep HOInfo x -> HOInfo) -> Generic HOInfo
forall x. Rep HOInfo x -> HOInfo
forall x. HOInfo -> Rep HOInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. HOInfo -> Rep HOInfo x
from :: forall x. HOInfo -> Rep HOInfo x
$cto :: forall x. Rep HOInfo x -> HOInfo
to :: forall x. Rep HOInfo x -> HOInfo
Generic)
allowHO, allowHOquals :: GInfo c a -> Bool
allowHO :: forall (c :: * -> *) a. GInfo c a -> Bool
allowHO = HOInfo -> Bool
hoBinds (HOInfo -> Bool) -> (GInfo c a -> HOInfo) -> GInfo c a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> HOInfo
forall (c :: * -> *) a. GInfo c a -> HOInfo
hoInfo
allowHOquals :: forall (c :: * -> *) a. GInfo c a -> Bool
allowHOquals = HOInfo -> Bool
hoQuals (HOInfo -> Bool) -> (GInfo c a -> HOInfo) -> GInfo c a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> HOInfo
forall (c :: * -> *) a. GInfo c a -> HOInfo
hoInfo
data GInfo c a = FI
{ forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm :: !(M.HashMap SubcId (c a))
, forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws :: !(M.HashMap KVar (WfC a))
, forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs :: !(BindEnv a)
, forall (c :: * -> *) a. GInfo c a -> Tag
ebinds :: ![BindId]
, forall (c :: * -> *) a. GInfo c a -> SEnv Sort
gLits :: !(SEnv Sort)
, forall (c :: * -> *) a. GInfo c a -> SEnv Sort
dLits :: !(SEnv Sort)
, forall (c :: * -> *) a. GInfo c a -> Kuts
kuts :: !Kuts
, forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals :: ![Qualifier]
, forall (c :: * -> *) a. GInfo c a -> HashMap Int a
bindInfo :: !(M.HashMap BindId a)
, forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls :: ![DataDecl]
, forall (c :: * -> *) a. GInfo c a -> HOInfo
hoInfo :: !HOInfo
, forall (c :: * -> *) a. GInfo c a -> [Triggered Expr]
asserts :: ![Triggered Expr]
, forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae :: AxiomEnv
}
deriving (GInfo c a -> GInfo c a -> Bool
(GInfo c a -> GInfo c a -> Bool)
-> (GInfo c a -> GInfo c a -> Bool) -> Eq (GInfo c a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (c :: * -> *) a.
(Eq a, Eq (c a)) =>
GInfo c a -> GInfo c a -> Bool
$c== :: forall (c :: * -> *) a.
(Eq a, Eq (c a)) =>
GInfo c a -> GInfo c a -> Bool
== :: GInfo c a -> GInfo c a -> Bool
$c/= :: forall (c :: * -> *) a.
(Eq a, Eq (c a)) =>
GInfo c a -> GInfo c a -> Bool
/= :: GInfo c a -> GInfo c a -> Bool
Eq, Int -> GInfo c a -> [Char] -> [Char]
[GInfo c a] -> [Char] -> [Char]
GInfo c a -> [Char]
(Int -> GInfo c a -> [Char] -> [Char])
-> (GInfo c a -> [Char])
-> ([GInfo c a] -> [Char] -> [Char])
-> Show (GInfo c a)
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
Int -> GInfo c a -> [Char] -> [Char]
forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
[GInfo c a] -> [Char] -> [Char]
forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
GInfo c a -> [Char]
$cshowsPrec :: forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
Int -> GInfo c a -> [Char] -> [Char]
showsPrec :: Int -> GInfo c a -> [Char] -> [Char]
$cshow :: forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
GInfo c a -> [Char]
show :: GInfo c a -> [Char]
$cshowList :: forall (c :: * -> *) a.
(Fixpoint a, Show a, Show (c a)) =>
[GInfo c a] -> [Char] -> [Char]
showList :: [GInfo c a] -> [Char] -> [Char]
Show, (forall a b. (a -> b) -> GInfo c a -> GInfo c b)
-> (forall a b. a -> GInfo c b -> GInfo c a) -> Functor (GInfo c)
forall a b. a -> GInfo c b -> GInfo c a
forall a b. (a -> b) -> GInfo c a -> GInfo c b
forall (c :: * -> *) a b. Functor c => a -> GInfo c b -> GInfo c a
forall (c :: * -> *) a b.
Functor c =>
(a -> b) -> GInfo c a -> GInfo c b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (c :: * -> *) a b.
Functor c =>
(a -> b) -> GInfo c a -> GInfo c b
fmap :: forall a b. (a -> b) -> GInfo c a -> GInfo c b
$c<$ :: forall (c :: * -> *) a b. Functor c => a -> GInfo c b -> GInfo c a
<$ :: forall a b. a -> GInfo c b -> GInfo c a
Functor, (forall x. GInfo c a -> Rep (GInfo c a) x)
-> (forall x. Rep (GInfo c a) x -> GInfo c a)
-> Generic (GInfo c a)
forall x. Rep (GInfo c a) x -> GInfo c a
forall x. GInfo c a -> Rep (GInfo c a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (c :: * -> *) a x. Rep (GInfo c a) x -> GInfo c a
forall (c :: * -> *) a x. GInfo c a -> Rep (GInfo c a) x
$cfrom :: forall (c :: * -> *) a x. GInfo c a -> Rep (GInfo c a) x
from :: forall x. GInfo c a -> Rep (GInfo c a) x
$cto :: forall (c :: * -> *) a x. Rep (GInfo c a) x -> GInfo c a
to :: forall x. Rep (GInfo c a) x -> GInfo c a
Generic)
instance HasGradual (GInfo c a) where
isGradual :: GInfo c a -> Bool
isGradual GInfo c a
info = (WfC a -> Bool) -> [WfC a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any WfC a -> Bool
forall a. HasGradual a => a -> Bool
isGradual (HashMap KVar (WfC a) -> [WfC a]
forall k v. HashMap k v -> [v]
M.elems (HashMap KVar (WfC a) -> [WfC a])
-> HashMap KVar (WfC a) -> [WfC a]
forall a b. (a -> b) -> a -> b
$ GInfo c a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws GInfo c a
info)
instance Semigroup HOInfo where
HOInfo
i1 <> :: HOInfo -> HOInfo -> HOInfo
<> HOInfo
i2 = HOI { hoBinds :: Bool
hoBinds = HOInfo -> Bool
hoBinds HOInfo
i1 Bool -> Bool -> Bool
|| HOInfo -> Bool
hoBinds HOInfo
i2
, hoQuals :: Bool
hoQuals = HOInfo -> Bool
hoQuals HOInfo
i1 Bool -> Bool -> Bool
|| HOInfo -> Bool
hoQuals HOInfo
i2
}
instance Monoid HOInfo where
mempty :: HOInfo
mempty = Bool -> Bool -> HOInfo
HOI Bool
False Bool
False
instance Semigroup (GInfo c a) where
GInfo c a
i1 <> :: GInfo c a -> GInfo c a -> GInfo c a
<> GInfo c a
i2 = FI { cm :: HashMap Integer (c a)
cm = GInfo c a -> HashMap Integer (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm GInfo c a
i1 HashMap Integer (c a)
-> HashMap Integer (c a) -> HashMap Integer (c a)
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> HashMap Integer (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm GInfo c a
i2
, ws :: HashMap KVar (WfC a)
ws = GInfo c a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws GInfo c a
i1 HashMap KVar (WfC a)
-> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws GInfo c a
i2
, bs :: BindEnv a
bs = GInfo c a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs GInfo c a
i1 BindEnv a -> BindEnv a -> BindEnv a
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs GInfo c a
i2
, ebinds :: Tag
ebinds = GInfo c a -> Tag
forall (c :: * -> *) a. GInfo c a -> Tag
ebinds GInfo c a
i1 Tag -> Tag -> Tag
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> Tag
forall (c :: * -> *) a. GInfo c a -> Tag
ebinds GInfo c a
i2
, gLits :: SEnv Sort
gLits = GInfo c a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
gLits GInfo c a
i1 SEnv Sort -> SEnv Sort -> SEnv Sort
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
gLits GInfo c a
i2
, dLits :: SEnv Sort
dLits = GInfo c a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
dLits GInfo c a
i1 SEnv Sort -> SEnv Sort -> SEnv Sort
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
dLits GInfo c a
i2
, kuts :: Kuts
kuts = GInfo c a -> Kuts
forall (c :: * -> *) a. GInfo c a -> Kuts
kuts GInfo c a
i1 Kuts -> Kuts -> Kuts
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> Kuts
forall (c :: * -> *) a. GInfo c a -> Kuts
kuts GInfo c a
i2
, quals :: [Qualifier]
quals = GInfo c a -> [Qualifier]
forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals GInfo c a
i1 [Qualifier] -> [Qualifier] -> [Qualifier]
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> [Qualifier]
forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals GInfo c a
i2
, bindInfo :: HashMap Int a
bindInfo = GInfo c a -> HashMap Int a
forall (c :: * -> *) a. GInfo c a -> HashMap Int a
bindInfo GInfo c a
i1 HashMap Int a -> HashMap Int a -> HashMap Int a
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> HashMap Int a
forall (c :: * -> *) a. GInfo c a -> HashMap Int a
bindInfo GInfo c a
i2
, ddecls :: [DataDecl]
ddecls = GInfo c a -> [DataDecl]
forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls GInfo c a
i1 [DataDecl] -> [DataDecl] -> [DataDecl]
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> [DataDecl]
forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls GInfo c a
i2
, hoInfo :: HOInfo
hoInfo = GInfo c a -> HOInfo
forall (c :: * -> *) a. GInfo c a -> HOInfo
hoInfo GInfo c a
i1 HOInfo -> HOInfo -> HOInfo
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> HOInfo
forall (c :: * -> *) a. GInfo c a -> HOInfo
hoInfo GInfo c a
i2
, asserts :: [Triggered Expr]
asserts = GInfo c a -> [Triggered Expr]
forall (c :: * -> *) a. GInfo c a -> [Triggered Expr]
asserts GInfo c a
i1 [Triggered Expr] -> [Triggered Expr] -> [Triggered Expr]
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> [Triggered Expr]
forall (c :: * -> *) a. GInfo c a -> [Triggered Expr]
asserts GInfo c a
i2
, ae :: AxiomEnv
ae = GInfo c a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae GInfo c a
i1 AxiomEnv -> AxiomEnv -> AxiomEnv
forall a. Semigroup a => a -> a -> a
<> GInfo c a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae GInfo c a
i2
}
instance Monoid (GInfo c a) where
mempty :: GInfo c a
mempty = FI { cm :: HashMap Integer (c a)
cm = HashMap Integer (c a)
forall k v. HashMap k v
M.empty
, ws :: HashMap KVar (WfC a)
ws = HashMap KVar (WfC a)
forall a. Monoid a => a
mempty
, bs :: BindEnv a
bs = BindEnv a
forall a. Monoid a => a
mempty
, ebinds :: Tag
ebinds = Tag
forall a. Monoid a => a
mempty
, gLits :: SEnv Sort
gLits = SEnv Sort
forall a. Monoid a => a
mempty
, dLits :: SEnv Sort
dLits = SEnv Sort
forall a. Monoid a => a
mempty
, kuts :: Kuts
kuts = Kuts
forall a. Monoid a => a
mempty
, quals :: [Qualifier]
quals = [Qualifier]
forall a. Monoid a => a
mempty
, bindInfo :: HashMap Int a
bindInfo = HashMap Int a
forall a. Monoid a => a
mempty
, ddecls :: [DataDecl]
ddecls = [DataDecl]
forall a. Monoid a => a
mempty
, hoInfo :: HOInfo
hoInfo = HOInfo
forall a. Monoid a => a
mempty
, asserts :: [Triggered Expr]
asserts = [Triggered Expr]
forall a. Monoid a => a
mempty
, ae :: AxiomEnv
ae = AxiomEnv
forall a. Monoid a => a
mempty
}
instance PTable (SInfo a) where
ptable :: SInfo a -> DocTable
ptable SInfo a
z = [(Doc, Doc)] -> DocTable
DocTable [ ([Char] -> Doc
text [Char]
"# Sub Constraints", Int -> Doc
forall a. PPrint a => a -> Doc
pprint (Int -> Doc) -> Int -> Doc
forall a b. (a -> b) -> a -> b
$ HashMap Integer (SimpC a) -> Int
forall a. HashMap Integer a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (HashMap Integer (SimpC a) -> Int)
-> HashMap Integer (SimpC a) -> Int
forall a b. (a -> b) -> a -> b
$ SInfo a -> HashMap Integer (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm SInfo a
z)
, ([Char] -> Doc
text [Char]
"# WF Constraints", Int -> Doc
forall a. PPrint a => a -> Doc
pprint (Int -> Doc) -> Int -> Doc
forall a b. (a -> b) -> a -> b
$ HashMap KVar (WfC a) -> Int
forall a. HashMap KVar a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (HashMap KVar (WfC a) -> Int) -> HashMap KVar (WfC a) -> Int
forall a b. (a -> b) -> a -> b
$ SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws SInfo a
z)
]
toFixpoint :: (Fixpoint a, Fixpoint (c a)) => Config -> GInfo c a -> Doc
toFixpoint :: forall a (c :: * -> *).
(Fixpoint a, Fixpoint (c a)) =>
Config -> GInfo c a -> Doc
toFixpoint Config
cfg GInfo c a
x' = Config -> Doc
forall a. Show a => a -> Doc
cfgDoc Config
cfg
Doc -> Doc -> Doc
$++$ GInfo c a -> Doc
forall {c :: * -> *} {a}. GInfo c a -> Doc
declsDoc GInfo c a
x'
Doc -> Doc -> Doc
$++$ GInfo c a -> Doc
forall {c :: * -> *} {a}. GInfo c a -> Doc
aeDoc GInfo c a
x'
Doc -> Doc -> Doc
$++$ GInfo c a -> Doc
forall {c :: * -> *} {a}. GInfo c a -> Doc
qualsDoc GInfo c a
x'
Doc -> Doc -> Doc
$++$ GInfo c a -> Doc
forall {c :: * -> *} {a}. GInfo c a -> Doc
kutsDoc GInfo c a
x'
Doc -> Doc -> Doc
$++$ GInfo c a -> Doc
forall {c :: * -> *} {a}. GInfo c a -> Doc
gConDoc GInfo c a
x'
Doc -> Doc -> Doc
$++$ GInfo c a -> Doc
forall {c :: * -> *} {a}. GInfo c a -> Doc
dConDoc GInfo c a
x'
Doc -> Doc -> Doc
$++$ Doc
bindsDoc
Doc -> Doc -> Doc
$++$ GInfo c a -> Doc
forall {c :: * -> *} {a}. Fixpoint (c a) => GInfo c a -> Doc
csDoc GInfo c a
x'
Doc -> Doc -> Doc
$++$ GInfo c a -> Doc
forall {a} {c :: * -> *}. Fixpoint a => GInfo c a -> Doc
wsDoc GInfo c a
x'
Doc -> Doc -> Doc
$++$ GInfo c a -> Doc
binfoDoc GInfo c a
x'
Doc -> Doc -> Doc
$++$ [Char] -> Doc
text [Char]
"\n"
where
cfgDoc :: a -> Doc
cfgDoc a
cfg = [Char] -> Doc
text ([Char]
"// " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
cfg)
gConDoc :: GInfo c a -> Doc
gConDoc = Doc -> SEnv Sort -> Doc
sEnvDoc Doc
"constant" (SEnv Sort -> Doc) -> (GInfo c a -> SEnv Sort) -> GInfo c a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
gLits
dConDoc :: GInfo c a -> Doc
dConDoc = Doc -> SEnv Sort -> Doc
sEnvDoc Doc
"distinct" (SEnv Sort -> Doc) -> (GInfo c a -> SEnv Sort) -> GInfo c a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
dLits
csDoc :: GInfo c a -> Doc
csDoc = [Doc] -> Doc
vcat ([Doc] -> Doc) -> (GInfo c a -> [Doc]) -> GInfo c a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Integer, c a) -> Doc) -> [(Integer, c a)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (c a -> Doc
forall a. Fixpoint a => a -> Doc
toFix (c a -> Doc) -> ((Integer, c a) -> c a) -> (Integer, c a) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer, c a) -> c a
forall a b. (a, b) -> b
snd) ([(Integer, c a)] -> [Doc])
-> (GInfo c a -> [(Integer, c a)]) -> GInfo c a -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Integer (c a) -> [(Integer, c a)]
forall a b. Ord a => HashMap a b -> [(a, b)]
hashMapToAscList (HashMap Integer (c a) -> [(Integer, c a)])
-> (GInfo c a -> HashMap Integer (c a))
-> GInfo c a
-> [(Integer, c a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> HashMap Integer (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm
wsDoc :: GInfo c a -> Doc
wsDoc = [Doc] -> Doc
vcat ([Doc] -> Doc) -> (GInfo c a -> [Doc]) -> GInfo c a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WfC a -> Doc) -> [WfC a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map WfC a -> Doc
forall a. Fixpoint a => a -> Doc
toFix ([WfC a] -> [Doc]) -> (GInfo c a -> [WfC a]) -> GInfo c a -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WfC a -> KVar) -> [WfC a] -> [WfC a]
forall b a. Ord b => (a -> b) -> [a] -> [a]
L.sortOn ((Symbol, Sort, KVar) -> KVar
forall a b c. (a, b, c) -> c
thd3 ((Symbol, Sort, KVar) -> KVar)
-> (WfC a -> (Symbol, Sort, KVar)) -> WfC a -> KVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WfC a -> (Symbol, Sort, KVar)
forall a. WfC a -> (Symbol, Sort, KVar)
wrft) ([WfC a] -> [WfC a])
-> (GInfo c a -> [WfC a]) -> GInfo c a -> [WfC a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap KVar (WfC a) -> [WfC a]
forall k v. HashMap k v -> [v]
M.elems (HashMap KVar (WfC a) -> [WfC a])
-> (GInfo c a -> HashMap KVar (WfC a)) -> GInfo c a -> [WfC a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws
kutsDoc :: GInfo c a -> Doc
kutsDoc = Kuts -> Doc
forall a. Fixpoint a => a -> Doc
toFix (Kuts -> Doc) -> (GInfo c a -> Kuts) -> GInfo c a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> Kuts
forall (c :: * -> *) a. GInfo c a -> Kuts
kuts
declsDoc :: GInfo c a -> Doc
declsDoc = [Doc] -> Doc
vcat ([Doc] -> Doc) -> (GInfo c a -> [Doc]) -> GInfo c a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataDecl -> Doc) -> [DataDecl] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (([Char] -> Doc
text [Char]
"data" Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> (DataDecl -> Doc) -> DataDecl -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDecl -> Doc
forall a. Fixpoint a => a -> Doc
toFix) ([DataDecl] -> [Doc])
-> (GInfo c a -> [DataDecl]) -> GInfo c a -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DataDecl] -> [DataDecl]
forall a. Ord a => [a] -> [a]
L.sort ([DataDecl] -> [DataDecl])
-> (GInfo c a -> [DataDecl]) -> GInfo c a -> [DataDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> [DataDecl]
forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls
(BindEnv a
ubs, EBindEnv a
ebs) = BindEnv a -> Tag -> (BindEnv a, EBindEnv a)
forall a. BindEnv a -> Tag -> (BindEnv a, EBindEnv a)
splitByQuantifiers (GInfo c a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs GInfo c a
x') (GInfo c a -> Tag
forall (c :: * -> *) a. GInfo c a -> Tag
ebinds GInfo c a
x')
bindsDoc :: Doc
bindsDoc = BindEnv a -> Doc
forall a. Fixpoint a => a -> Doc
toFix BindEnv a
ubs
Doc -> Doc -> Doc
$++$ EBindEnv a -> Doc
forall a. Fixpoint a => a -> Doc
toFix EBindEnv a
ebs
qualsDoc :: GInfo c a -> Doc
qualsDoc = [Doc] -> Doc
vcat ([Doc] -> Doc) -> (GInfo c a -> [Doc]) -> GInfo c a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Qualifier -> Doc) -> [Qualifier] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Qualifier -> Doc
forall a. Fixpoint a => a -> Doc
toFix ([Qualifier] -> [Doc])
-> (GInfo c a -> [Qualifier]) -> GInfo c a -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Qualifier] -> [Qualifier]
forall a. Ord a => [a] -> [a]
L.sort ([Qualifier] -> [Qualifier])
-> (GInfo c a -> [Qualifier]) -> GInfo c a -> [Qualifier]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> [Qualifier]
forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals
aeDoc :: GInfo c a -> Doc
aeDoc = AxiomEnv -> Doc
forall a. Fixpoint a => a -> Doc
toFix (AxiomEnv -> Doc) -> (GInfo c a -> AxiomEnv) -> GInfo c a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae
metaDoc :: (a, a) -> Doc
metaDoc (a
i,a
d) = Doc -> Doc -> Doc
toFixMeta ([Char] -> Doc
text [Char]
"bind" Doc -> Doc -> Doc
<+> a -> Doc
forall a. Fixpoint a => a -> Doc
toFix a
i) (a -> Doc
forall a. Fixpoint a => a -> Doc
toFix a
d)
mdata :: Bool
mdata = Config -> Bool
metadata Config
cfg
binfoDoc :: GInfo c a -> Doc
binfoDoc
| Bool
mdata = [Doc] -> Doc
vcat ([Doc] -> Doc) -> (GInfo c a -> [Doc]) -> GInfo c a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, a) -> Doc) -> [(Int, a)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int, a) -> Doc
forall {a} {a}. (Fixpoint a, Fixpoint a) => (a, a) -> Doc
metaDoc ([(Int, a)] -> [Doc])
-> (GInfo c a -> [(Int, a)]) -> GInfo c a -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Int a -> [(Int, a)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Int a -> [(Int, a)])
-> (GInfo c a -> HashMap Int a) -> GInfo c a -> [(Int, a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> HashMap Int a
forall (c :: * -> *) a. GInfo c a -> HashMap Int a
bindInfo
| Bool
otherwise = \GInfo c a
_ -> [Char] -> Doc
text [Char]
"\n"
infixl 9 $++$
($++$) :: Doc -> Doc -> Doc
Doc
x $++$ :: Doc -> Doc -> Doc
$++$ Doc
y = Doc
x Doc -> Doc -> Doc
$+$ [Char] -> Doc
text [Char]
"\n" Doc -> Doc -> Doc
$+$ Doc
y
sEnvDoc :: Doc -> SEnv Sort -> Doc
sEnvDoc :: Doc -> SEnv Sort -> Doc
sEnvDoc Doc
d = [Doc] -> Doc
vcat ([Doc] -> Doc) -> (SEnv Sort -> [Doc]) -> SEnv Sort -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Symbol, Sort) -> Doc) -> [(Symbol, Sort)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Doc
kvD ([(Symbol, Sort)] -> [Doc])
-> (SEnv Sort -> [(Symbol, Sort)]) -> SEnv Sort -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
L.sortOn (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst ([(Symbol, Sort)] -> [(Symbol, Sort)])
-> (SEnv Sort -> [(Symbol, Sort)]) -> SEnv Sort -> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SEnv Sort -> [(Symbol, Sort)]
forall a. SEnv a -> [(Symbol, a)]
toListSEnv
where
kvD :: (Symbol, Sort) -> Doc
kvD (Symbol
c, Sort
so) = Doc
d Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
c Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
so)
writeFInfo :: (Fixpoint a, Fixpoint (c a)) => Config -> GInfo c a -> FilePath -> IO ()
writeFInfo :: forall a (c :: * -> *).
(Fixpoint a, Fixpoint (c a)) =>
Config -> GInfo c a -> [Char] -> IO ()
writeFInfo Config
cfg GInfo c a
fq [Char]
f = [Char] -> [Char] -> IO ()
writeFile [Char]
f (Doc -> [Char]
render (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ Config -> GInfo c a -> Doc
forall a (c :: * -> *).
(Fixpoint a, Fixpoint (c a)) =>
Config -> GInfo c a -> Doc
toFixpoint Config
cfg GInfo c a
fq)
convertFormat :: (Fixpoint a) => FInfo a -> SInfo a
convertFormat :: forall a. Fixpoint a => FInfo a -> SInfo a
convertFormat FInfo a
fi = FInfo a
fi' { cm = subcToSimpc bindm <$> cm fi' }
where
(BindM
bindm, FInfo a
fi') = ((BindM, FInfo a) -> Integer -> SubC a -> (BindM, FInfo a))
-> (BindM, FInfo a) -> HashMap Integer (SubC a) -> (BindM, FInfo a)
forall a k v. (a -> k -> v -> a) -> a -> HashMap k v -> a
M.foldlWithKey' (BindM, FInfo a) -> Integer -> SubC a -> (BindM, FInfo a)
forall a. (BindM, FInfo a) -> Integer -> SubC a -> (BindM, FInfo a)
outVV (BindM
forall k v. HashMap k v
M.empty, FInfo a
fi) (HashMap Integer (SubC a) -> (BindM, FInfo a))
-> HashMap Integer (SubC a) -> (BindM, FInfo a)
forall a b. (a -> b) -> a -> b
$ FInfo a -> HashMap Integer (SubC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm FInfo a
fi
subcToSimpc :: BindM -> SubC a -> SimpC a
subcToSimpc :: forall a. BindM -> SubC a -> SimpC a
subcToSimpc BindM
m SubC a
s = SimpC
{ _cenv :: IBindEnv
_cenv = SubC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
s
, _crhs :: Expr
_crhs = Reft -> Expr
reftPred (Reft -> Expr) -> Reft -> Expr
forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft (SortedReft -> Reft) -> SortedReft -> Reft
forall a b. (a -> b) -> a -> b
$ SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs SubC a
s
, _cid :: Maybe Integer
_cid = SubC a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
sid SubC a
s
, cbind :: Int
cbind = [Char] -> Integer -> BindM -> Int
forall k v.
(?callStack::CallStack, Eq k, Hashable k) =>
[Char] -> k -> HashMap k v -> v
safeLookup [Char]
"subcToSimpc" (SubC a -> Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Integer
subcId SubC a
s) BindM
m
, _ctag :: Tag
_ctag = SubC a -> Tag
forall (c :: * -> *) a. TaggedC c a => c a -> Tag
stag SubC a
s
, _cinfo :: a
_cinfo = SubC a -> a
forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SubC a
s
}
outVV :: (BindM, FInfo a) -> Integer -> SubC a -> (BindM, FInfo a)
outVV :: forall a. (BindM, FInfo a) -> Integer -> SubC a -> (BindM, FInfo a)
outVV (BindM
m, FInfo a
fi) Integer
i SubC a
c = (BindM
m', FInfo a
fi')
where
fi' :: FInfo a
fi' = FInfo a
fi { bs = be', cm = cm' }
m' :: BindM
m' = Integer -> Int -> BindM -> BindM
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Integer
i Int
bId BindM
m
(Int
bId, BindEnv a
be') = Symbol -> SortedReft -> a -> BindEnv a -> (Int, BindEnv a)
forall a.
Symbol -> SortedReft -> a -> BindEnv a -> (Int, BindEnv a)
insertBindEnv Symbol
x SortedReft
sr (SubC a -> a
forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SubC a
c) (FInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs FInfo a
fi)
cm' :: HashMap Integer (SubC a)
cm' = Integer
-> SubC a -> HashMap Integer (SubC a) -> HashMap Integer (SubC a)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Integer
i SubC a
c' (HashMap Integer (SubC a) -> HashMap Integer (SubC a))
-> HashMap Integer (SubC a) -> HashMap Integer (SubC a)
forall a b. (a -> b) -> a -> b
$ FInfo a -> HashMap Integer (SubC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm FInfo a
fi
c' :: SubC a
c' = SubC a
c { _senv = insertsIBindEnv [bId] $ senv c }
sr :: SortedReft
sr = SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
c
x :: Symbol
x = Reft -> Symbol
reftBind (Reft -> Symbol) -> Reft -> Symbol
forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft SortedReft
sr
type BindM = M.HashMap Integer BindId
sinfoToFInfo :: SInfo a -> FInfo a
sinfoToFInfo :: forall a. SInfo a -> FInfo a
sinfoToFInfo SInfo a
fi = SInfo a
fi
{ bs = envWithoutLhss
, cm = simpcToSubc (bs fi) <$> cm fi
}
where
envWithoutLhss :: BindEnv a
envWithoutLhss =
(BindEnv a -> SimpC a -> BindEnv a)
-> BindEnv a -> HashMap Integer (SimpC a) -> BindEnv a
forall a v k. (a -> v -> a) -> a -> HashMap k v -> a
M.foldl' (\BindEnv a
m SimpC a
c -> Int -> BindEnv a -> BindEnv a
forall a. Int -> BindEnv a -> BindEnv a
deleteBindEnv (SimpC a -> Int
forall a. SimpC a -> Int
cbind SimpC a
c) BindEnv a
m) (SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi) (SInfo a -> HashMap Integer (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm SInfo a
fi)
simpcToSubc :: BindEnv a -> SimpC a -> SubC a
simpcToSubc :: forall a. BindEnv a -> SimpC a -> SubC a
simpcToSubc BindEnv a
env SimpC a
s = SubC
{ _senv :: IBindEnv
_senv = Int -> IBindEnv -> IBindEnv
deleteIBindEnv (SimpC a -> Int
forall a. SimpC a -> Int
cbind SimpC a
s) (SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC a
s)
, slhs :: SortedReft
slhs = SortedReft
sr
, srhs :: SortedReft
srhs = Sort -> Reft -> SortedReft
RR (SortedReft -> Sort
sr_sort SortedReft
sr) ((Symbol, Expr) -> Reft
Reft (Symbol
b, SimpC a -> Expr
forall a. SimpC a -> Expr
_crhs SimpC a
s))
, _sid :: Maybe Integer
_sid = SimpC a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
sid SimpC a
s
, _stag :: Tag
_stag = SimpC a -> Tag
forall (c :: * -> *) a. TaggedC c a => c a -> Tag
stag SimpC a
s
, _sinfo :: a
_sinfo = SimpC a -> a
forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SimpC a
s
}
where
(Symbol
b, SortedReft
sr, a
_) = Int -> BindEnv a -> (Symbol, SortedReft, a)
forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv (SimpC a -> Int
forall a. SimpC a -> Int
cbind SimpC a
s) BindEnv a
env
type Solver a = Config -> FInfo a -> IO (Result (Integer, a))
saveQuery :: (Fixpoint a) => Config -> FInfo a -> IO ()
saveQuery :: forall a. Fixpoint a => Config -> FInfo a -> IO ()
saveQuery Config
cfg FInfo a
fi = do
let fi' :: FInfo ()
fi' = FInfo a -> FInfo ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void FInfo a
fi
Config -> FInfo () -> IO ()
saveBinaryQuery Config
cfg FInfo ()
fi'
Config -> FInfo a -> IO ()
forall a. Fixpoint a => Config -> FInfo a -> IO ()
saveTextQuery Config
cfg FInfo a
fi
saveBinaryQuery :: Config -> FInfo () -> IO ()
saveBinaryQuery :: Config -> FInfo () -> IO ()
saveBinaryQuery Config
cfg FInfo ()
fi = do
let bfq :: [Char]
bfq = Ext -> Config -> [Char]
queryFile Ext
Files.BinFq Config
cfg
[Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Saving Binary Query: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
bfq [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
[Char] -> IO ()
ensurePath [Char]
bfq
[Char] -> ByteString -> IO ()
B.writeFile [Char]
bfq (FInfo () -> ByteString
forall a. Store a => a -> ByteString
S.encode FInfo ()
fi)
saveTextQuery :: Fixpoint a => Config -> FInfo a -> IO ()
saveTextQuery :: forall a. Fixpoint a => Config -> FInfo a -> IO ()
saveTextQuery Config
cfg FInfo a
fi = do
let fq :: [Char]
fq = Ext -> Config -> [Char]
queryFile Ext
Files.Fq Config
cfg
[Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Saving Text Query: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
fq [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
[Char] -> IO ()
ensurePath [Char]
fq
[Char] -> [Char] -> IO ()
writeFile [Char]
fq ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
render (Config -> FInfo a -> Doc
forall a (c :: * -> *).
(Fixpoint a, Fixpoint (c a)) =>
Config -> GInfo c a -> Doc
toFixpoint Config
cfg FInfo a
fi)
data AxiomEnv = AEnv
{ AxiomEnv -> [Equation]
aenvEqs :: ![Equation]
, AxiomEnv -> [Rewrite]
aenvSimpl :: ![Rewrite]
, AxiomEnv -> HashMap Integer Bool
aenvExpand :: M.HashMap SubcId Bool
, AxiomEnv -> HashMap Integer [AutoRewrite]
aenvAutoRW :: M.HashMap SubcId [AutoRewrite]
} deriving (AxiomEnv -> AxiomEnv -> Bool
(AxiomEnv -> AxiomEnv -> Bool)
-> (AxiomEnv -> AxiomEnv -> Bool) -> Eq AxiomEnv
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AxiomEnv -> AxiomEnv -> Bool
== :: AxiomEnv -> AxiomEnv -> Bool
$c/= :: AxiomEnv -> AxiomEnv -> Bool
/= :: AxiomEnv -> AxiomEnv -> Bool
Eq, Int -> AxiomEnv -> [Char] -> [Char]
[AxiomEnv] -> [Char] -> [Char]
AxiomEnv -> [Char]
(Int -> AxiomEnv -> [Char] -> [Char])
-> (AxiomEnv -> [Char])
-> ([AxiomEnv] -> [Char] -> [Char])
-> Show AxiomEnv
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> AxiomEnv -> [Char] -> [Char]
showsPrec :: Int -> AxiomEnv -> [Char] -> [Char]
$cshow :: AxiomEnv -> [Char]
show :: AxiomEnv -> [Char]
$cshowList :: [AxiomEnv] -> [Char] -> [Char]
showList :: [AxiomEnv] -> [Char] -> [Char]
Show, (forall x. AxiomEnv -> Rep AxiomEnv x)
-> (forall x. Rep AxiomEnv x -> AxiomEnv) -> Generic AxiomEnv
forall x. Rep AxiomEnv x -> AxiomEnv
forall x. AxiomEnv -> Rep AxiomEnv x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AxiomEnv -> Rep AxiomEnv x
from :: forall x. AxiomEnv -> Rep AxiomEnv x
$cto :: forall x. Rep AxiomEnv x -> AxiomEnv
to :: forall x. Rep AxiomEnv x -> AxiomEnv
Generic)
instance S.Store AutoRewrite
instance S.Store AxiomEnv
instance S.Store Rewrite
instance S.Store Equation
instance NFData AutoRewrite
instance NFData AxiomEnv
instance NFData Rewrite
instance NFData Equation
dedupAutoRewrites :: M.HashMap SubcId [AutoRewrite] -> [AutoRewrite]
dedupAutoRewrites :: HashMap Integer [AutoRewrite] -> [AutoRewrite]
dedupAutoRewrites = Set AutoRewrite -> [AutoRewrite]
forall a. Set a -> [a]
Set.toList (Set AutoRewrite -> [AutoRewrite])
-> (HashMap Integer [AutoRewrite] -> Set AutoRewrite)
-> HashMap Integer [AutoRewrite]
-> [AutoRewrite]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Set AutoRewrite] -> Set AutoRewrite
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set AutoRewrite] -> Set AutoRewrite)
-> (HashMap Integer [AutoRewrite] -> [Set AutoRewrite])
-> HashMap Integer [AutoRewrite]
-> Set AutoRewrite
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([AutoRewrite] -> Set AutoRewrite)
-> [[AutoRewrite]] -> [Set AutoRewrite]
forall a b. (a -> b) -> [a] -> [b]
map [AutoRewrite] -> Set AutoRewrite
forall a. Ord a => [a] -> Set a
Set.fromList ([[AutoRewrite]] -> [Set AutoRewrite])
-> (HashMap Integer [AutoRewrite] -> [[AutoRewrite]])
-> HashMap Integer [AutoRewrite]
-> [Set AutoRewrite]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Integer [AutoRewrite] -> [[AutoRewrite]]
forall k v. HashMap k v -> [v]
M.elems
instance Semigroup AxiomEnv where
AxiomEnv
a1 <> :: AxiomEnv -> AxiomEnv -> AxiomEnv
<> AxiomEnv
a2 = [Equation]
-> [Rewrite]
-> HashMap Integer Bool
-> HashMap Integer [AutoRewrite]
-> AxiomEnv
AEnv [Equation]
aenvEqs' [Rewrite]
aenvSimpl' HashMap Integer Bool
aenvExpand' HashMap Integer [AutoRewrite]
aenvAutoRW'
where
aenvEqs' :: [Equation]
aenvEqs' = AxiomEnv -> [Equation]
aenvEqs AxiomEnv
a1 [Equation] -> [Equation] -> [Equation]
forall a. Semigroup a => a -> a -> a
<> AxiomEnv -> [Equation]
aenvEqs AxiomEnv
a2
aenvSimpl' :: [Rewrite]
aenvSimpl' = AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
a1 [Rewrite] -> [Rewrite] -> [Rewrite]
forall a. Semigroup a => a -> a -> a
<> AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
a2
aenvExpand' :: HashMap Integer Bool
aenvExpand' = AxiomEnv -> HashMap Integer Bool
aenvExpand AxiomEnv
a1 HashMap Integer Bool
-> HashMap Integer Bool -> HashMap Integer Bool
forall a. Semigroup a => a -> a -> a
<> AxiomEnv -> HashMap Integer Bool
aenvExpand AxiomEnv
a2
aenvAutoRW' :: HashMap Integer [AutoRewrite]
aenvAutoRW' = AxiomEnv -> HashMap Integer [AutoRewrite]
aenvAutoRW AxiomEnv
a1 HashMap Integer [AutoRewrite]
-> HashMap Integer [AutoRewrite] -> HashMap Integer [AutoRewrite]
forall a. Semigroup a => a -> a -> a
<> AxiomEnv -> HashMap Integer [AutoRewrite]
aenvAutoRW AxiomEnv
a2
instance Monoid AxiomEnv where
mempty :: AxiomEnv
mempty = [Equation]
-> [Rewrite]
-> HashMap Integer Bool
-> HashMap Integer [AutoRewrite]
-> AxiomEnv
AEnv [] [] ([(Integer, Bool)] -> HashMap Integer Bool
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList []) ([(Integer, [AutoRewrite])] -> HashMap Integer [AutoRewrite]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [])
mappend :: AxiomEnv -> AxiomEnv -> AxiomEnv
mappend = AxiomEnv -> AxiomEnv -> AxiomEnv
forall a. Semigroup a => a -> a -> a
(<>)
instance PPrint AxiomEnv where
pprintTidy :: Tidy -> AxiomEnv -> Doc
pprintTidy Tidy
_ = [Char] -> Doc
text ([Char] -> Doc) -> (AxiomEnv -> [Char]) -> AxiomEnv -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AxiomEnv -> [Char]
forall a. Show a => a -> [Char]
show
data Equation = Equ
{ Equation -> Symbol
eqName :: !Symbol
, Equation -> [(Symbol, Sort)]
eqArgs :: [(Symbol, Sort)]
, Equation -> Expr
eqBody :: !Expr
, Equation -> Sort
eqSort :: !Sort
, Equation -> Bool
eqRec :: !Bool
}
deriving (Typeable Equation
Typeable Equation =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Equation -> c Equation)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Equation)
-> (Equation -> Constr)
-> (Equation -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Equation))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Equation))
-> ((forall b. Data b => b -> b) -> Equation -> Equation)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Equation -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Equation -> r)
-> (forall u. (forall d. Data d => d -> u) -> Equation -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Equation -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation)
-> Data Equation
Equation -> Constr
Equation -> DataType
(forall b. Data b => b -> b) -> Equation -> Equation
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Equation -> u
forall u. (forall d. Data d => d -> u) -> Equation -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Equation -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Equation -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Equation
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Equation -> c Equation
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Equation)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Equation)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Equation -> c Equation
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Equation -> c Equation
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Equation
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Equation
$ctoConstr :: Equation -> Constr
toConstr :: Equation -> Constr
$cdataTypeOf :: Equation -> DataType
dataTypeOf :: Equation -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Equation)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Equation)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Equation)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Equation)
$cgmapT :: (forall b. Data b => b -> b) -> Equation -> Equation
gmapT :: (forall b. Data b => b -> b) -> Equation -> Equation
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Equation -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Equation -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Equation -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Equation -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Equation -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Equation -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Equation -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Equation -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Equation -> m Equation
Data, Equation -> Equation -> Bool
(Equation -> Equation -> Bool)
-> (Equation -> Equation -> Bool) -> Eq Equation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Equation -> Equation -> Bool
== :: Equation -> Equation -> Bool
$c/= :: Equation -> Equation -> Bool
/= :: Equation -> Equation -> Bool
Eq, Eq Equation
Eq Equation =>
(Equation -> Equation -> Ordering)
-> (Equation -> Equation -> Bool)
-> (Equation -> Equation -> Bool)
-> (Equation -> Equation -> Bool)
-> (Equation -> Equation -> Bool)
-> (Equation -> Equation -> Equation)
-> (Equation -> Equation -> Equation)
-> Ord Equation
Equation -> Equation -> Bool
Equation -> Equation -> Ordering
Equation -> Equation -> Equation
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Equation -> Equation -> Ordering
compare :: Equation -> Equation -> Ordering
$c< :: Equation -> Equation -> Bool
< :: Equation -> Equation -> Bool
$c<= :: Equation -> Equation -> Bool
<= :: Equation -> Equation -> Bool
$c> :: Equation -> Equation -> Bool
> :: Equation -> Equation -> Bool
$c>= :: Equation -> Equation -> Bool
>= :: Equation -> Equation -> Bool
$cmax :: Equation -> Equation -> Equation
max :: Equation -> Equation -> Equation
$cmin :: Equation -> Equation -> Equation
min :: Equation -> Equation -> Equation
Ord, Int -> Equation -> [Char] -> [Char]
[Equation] -> [Char] -> [Char]
Equation -> [Char]
(Int -> Equation -> [Char] -> [Char])
-> (Equation -> [Char])
-> ([Equation] -> [Char] -> [Char])
-> Show Equation
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> Equation -> [Char] -> [Char]
showsPrec :: Int -> Equation -> [Char] -> [Char]
$cshow :: Equation -> [Char]
show :: Equation -> [Char]
$cshowList :: [Equation] -> [Char] -> [Char]
showList :: [Equation] -> [Char] -> [Char]
Show, (forall x. Equation -> Rep Equation x)
-> (forall x. Rep Equation x -> Equation) -> Generic Equation
forall x. Rep Equation x -> Equation
forall x. Equation -> Rep Equation x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Equation -> Rep Equation x
from :: forall x. Equation -> Rep Equation x
$cto :: forall x. Rep Equation x -> Equation
to :: forall x. Rep Equation x -> Equation
Generic)
mkEquation :: Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
mkEquation :: Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
mkEquation Symbol
f [(Symbol, Sort)]
xts Expr
e Sort
out = Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Bool -> Equation
Equ Symbol
f [(Symbol, Sort)]
xts Expr
e Sort
out (Symbol
f Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms Expr
e)
instance Subable Equation where
syms :: Equation -> [Symbol]
syms Equation
a = Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms (Equation -> Expr
eqBody Equation
a)
subst :: Subst -> Equation -> Equation
subst Subst
su = (Expr -> Expr) -> Equation -> Equation
mapEqBody (Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
subst Subst
su)
substf :: (Symbol -> Expr) -> Equation -> Equation
substf Symbol -> Expr
f = (Expr -> Expr) -> Equation -> Equation
mapEqBody ((Symbol -> Expr) -> Expr -> Expr
forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f)
substa :: (Symbol -> Symbol) -> Equation -> Equation
substa Symbol -> Symbol
f = (Expr -> Expr) -> Equation -> Equation
mapEqBody ((Symbol -> Symbol) -> Expr -> Expr
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
f)
mapEqBody :: (Expr -> Expr) -> Equation -> Equation
mapEqBody :: (Expr -> Expr) -> Equation -> Equation
mapEqBody Expr -> Expr
f Equation
a = Equation
a { eqBody = f (eqBody a) }
instance PPrint Equation where
pprintTidy :: Tidy -> Equation -> Doc
pprintTidy Tidy
_ = Equation -> Doc
forall a. Fixpoint a => a -> Doc
toFix
ppArgs :: (PPrint a) => [a] -> Doc
ppArgs :: forall a. PPrint a => [a] -> Doc
ppArgs = Doc -> Doc
parens (Doc -> Doc) -> ([a] -> Doc) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> Doc
intersperse Doc
", " ([Doc] -> Doc) -> ([a] -> [Doc]) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Doc
forall a. PPrint a => a -> Doc
pprint
data AutoRewrite = AutoRewrite
{ AutoRewrite -> [SortedReft]
arArgs :: [SortedReft]
, AutoRewrite -> Expr
arLHS :: Expr
, AutoRewrite -> Expr
arRHS :: Expr
} deriving (AutoRewrite -> AutoRewrite -> Bool
(AutoRewrite -> AutoRewrite -> Bool)
-> (AutoRewrite -> AutoRewrite -> Bool) -> Eq AutoRewrite
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AutoRewrite -> AutoRewrite -> Bool
== :: AutoRewrite -> AutoRewrite -> Bool
$c/= :: AutoRewrite -> AutoRewrite -> Bool
/= :: AutoRewrite -> AutoRewrite -> Bool
Eq, Eq AutoRewrite
Eq AutoRewrite =>
(AutoRewrite -> AutoRewrite -> Ordering)
-> (AutoRewrite -> AutoRewrite -> Bool)
-> (AutoRewrite -> AutoRewrite -> Bool)
-> (AutoRewrite -> AutoRewrite -> Bool)
-> (AutoRewrite -> AutoRewrite -> Bool)
-> (AutoRewrite -> AutoRewrite -> AutoRewrite)
-> (AutoRewrite -> AutoRewrite -> AutoRewrite)
-> Ord AutoRewrite
AutoRewrite -> AutoRewrite -> Bool
AutoRewrite -> AutoRewrite -> Ordering
AutoRewrite -> AutoRewrite -> AutoRewrite
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: AutoRewrite -> AutoRewrite -> Ordering
compare :: AutoRewrite -> AutoRewrite -> Ordering
$c< :: AutoRewrite -> AutoRewrite -> Bool
< :: AutoRewrite -> AutoRewrite -> Bool
$c<= :: AutoRewrite -> AutoRewrite -> Bool
<= :: AutoRewrite -> AutoRewrite -> Bool
$c> :: AutoRewrite -> AutoRewrite -> Bool
> :: AutoRewrite -> AutoRewrite -> Bool
$c>= :: AutoRewrite -> AutoRewrite -> Bool
>= :: AutoRewrite -> AutoRewrite -> Bool
$cmax :: AutoRewrite -> AutoRewrite -> AutoRewrite
max :: AutoRewrite -> AutoRewrite -> AutoRewrite
$cmin :: AutoRewrite -> AutoRewrite -> AutoRewrite
min :: AutoRewrite -> AutoRewrite -> AutoRewrite
Ord, Int -> AutoRewrite -> [Char] -> [Char]
[AutoRewrite] -> [Char] -> [Char]
AutoRewrite -> [Char]
(Int -> AutoRewrite -> [Char] -> [Char])
-> (AutoRewrite -> [Char])
-> ([AutoRewrite] -> [Char] -> [Char])
-> Show AutoRewrite
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> AutoRewrite -> [Char] -> [Char]
showsPrec :: Int -> AutoRewrite -> [Char] -> [Char]
$cshow :: AutoRewrite -> [Char]
show :: AutoRewrite -> [Char]
$cshowList :: [AutoRewrite] -> [Char] -> [Char]
showList :: [AutoRewrite] -> [Char] -> [Char]
Show, (forall x. AutoRewrite -> Rep AutoRewrite x)
-> (forall x. Rep AutoRewrite x -> AutoRewrite)
-> Generic AutoRewrite
forall x. Rep AutoRewrite x -> AutoRewrite
forall x. AutoRewrite -> Rep AutoRewrite x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AutoRewrite -> Rep AutoRewrite x
from :: forall x. AutoRewrite -> Rep AutoRewrite x
$cto :: forall x. Rep AutoRewrite x -> AutoRewrite
to :: forall x. Rep AutoRewrite x -> AutoRewrite
Generic)
instance Hashable AutoRewrite
instance Fixpoint (M.HashMap SubcId [AutoRewrite]) where
toFix :: HashMap Integer [AutoRewrite] -> Doc
toFix HashMap Integer [AutoRewrite]
autoRW =
[Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
(AutoRewrite -> Doc) -> [AutoRewrite] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map AutoRewrite -> Doc
fixRW [AutoRewrite]
rewrites [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
[Doc]
rwsMapping
where
rewrites :: [AutoRewrite]
rewrites = HashMap Integer [AutoRewrite] -> [AutoRewrite]
dedupAutoRewrites HashMap Integer [AutoRewrite]
autoRW
fixRW :: AutoRewrite -> Doc
fixRW rw :: AutoRewrite
rw@(AutoRewrite [SortedReft]
args Expr
lhs Expr
rhs) =
[Char] -> Doc
text ([Char]
"autorewrite " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (AutoRewrite -> Int
forall a. Hashable a => a -> Int
hash AutoRewrite
rw))
Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep ((SortedReft -> Doc) -> [SortedReft] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SortedReft -> Doc
forall a. Fixpoint a => a -> Doc
toFix [SortedReft]
args)
Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"="
Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"{"
Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix Expr
lhs
Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"="
Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix Expr
rhs
Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"}"
rwsMapping :: [Doc]
rwsMapping = do
(Integer
cid, [AutoRewrite]
rws) <- HashMap Integer [AutoRewrite] -> [(Integer, [AutoRewrite])]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Integer [AutoRewrite]
autoRW
AutoRewrite
rw <- [AutoRewrite]
rws
Doc -> [Doc]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> [Doc]) -> Doc -> [Doc]
forall a b. (a -> b) -> a -> b
$ Doc
"rewrite" Doc -> Doc -> Doc
<+> Doc -> Doc
brackets ([Char] -> Doc
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
cid [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (AutoRewrite -> Int
forall a. Hashable a => a -> Int
hash AutoRewrite
rw))
data Rewrite = SMeasure
{ Rewrite -> Symbol
smName :: Symbol
, Rewrite -> Symbol
smDC :: Symbol
, Rewrite -> [Symbol]
smArgs :: [Symbol]
, Rewrite -> Expr
smBody :: Expr
}
deriving (Typeable Rewrite
Typeable Rewrite =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rewrite -> c Rewrite)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Rewrite)
-> (Rewrite -> Constr)
-> (Rewrite -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Rewrite))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Rewrite))
-> ((forall b. Data b => b -> b) -> Rewrite -> Rewrite)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Rewrite -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Rewrite -> r)
-> (forall u. (forall d. Data d => d -> u) -> Rewrite -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Rewrite -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite)
-> Data Rewrite
Rewrite -> Constr
Rewrite -> DataType
(forall b. Data b => b -> b) -> Rewrite -> Rewrite
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Rewrite -> u
forall u. (forall d. Data d => d -> u) -> Rewrite -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Rewrite -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Rewrite -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Rewrite
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rewrite -> c Rewrite
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Rewrite)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Rewrite)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rewrite -> c Rewrite
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rewrite -> c Rewrite
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Rewrite
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Rewrite
$ctoConstr :: Rewrite -> Constr
toConstr :: Rewrite -> Constr
$cdataTypeOf :: Rewrite -> DataType
dataTypeOf :: Rewrite -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Rewrite)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Rewrite)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Rewrite)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Rewrite)
$cgmapT :: (forall b. Data b => b -> b) -> Rewrite -> Rewrite
gmapT :: (forall b. Data b => b -> b) -> Rewrite -> Rewrite
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Rewrite -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Rewrite -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Rewrite -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Rewrite -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Rewrite -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Rewrite -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Rewrite -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Rewrite -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rewrite -> m Rewrite
Data, Rewrite -> Rewrite -> Bool
(Rewrite -> Rewrite -> Bool)
-> (Rewrite -> Rewrite -> Bool) -> Eq Rewrite
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Rewrite -> Rewrite -> Bool
== :: Rewrite -> Rewrite -> Bool
$c/= :: Rewrite -> Rewrite -> Bool
/= :: Rewrite -> Rewrite -> Bool
Eq, Eq Rewrite
Eq Rewrite =>
(Rewrite -> Rewrite -> Ordering)
-> (Rewrite -> Rewrite -> Bool)
-> (Rewrite -> Rewrite -> Bool)
-> (Rewrite -> Rewrite -> Bool)
-> (Rewrite -> Rewrite -> Bool)
-> (Rewrite -> Rewrite -> Rewrite)
-> (Rewrite -> Rewrite -> Rewrite)
-> Ord Rewrite
Rewrite -> Rewrite -> Bool
Rewrite -> Rewrite -> Ordering
Rewrite -> Rewrite -> Rewrite
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Rewrite -> Rewrite -> Ordering
compare :: Rewrite -> Rewrite -> Ordering
$c< :: Rewrite -> Rewrite -> Bool
< :: Rewrite -> Rewrite -> Bool
$c<= :: Rewrite -> Rewrite -> Bool
<= :: Rewrite -> Rewrite -> Bool
$c> :: Rewrite -> Rewrite -> Bool
> :: Rewrite -> Rewrite -> Bool
$c>= :: Rewrite -> Rewrite -> Bool
>= :: Rewrite -> Rewrite -> Bool
$cmax :: Rewrite -> Rewrite -> Rewrite
max :: Rewrite -> Rewrite -> Rewrite
$cmin :: Rewrite -> Rewrite -> Rewrite
min :: Rewrite -> Rewrite -> Rewrite
Ord, Int -> Rewrite -> [Char] -> [Char]
[Rewrite] -> [Char] -> [Char]
Rewrite -> [Char]
(Int -> Rewrite -> [Char] -> [Char])
-> (Rewrite -> [Char])
-> ([Rewrite] -> [Char] -> [Char])
-> Show Rewrite
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> Rewrite -> [Char] -> [Char]
showsPrec :: Int -> Rewrite -> [Char] -> [Char]
$cshow :: Rewrite -> [Char]
show :: Rewrite -> [Char]
$cshowList :: [Rewrite] -> [Char] -> [Char]
showList :: [Rewrite] -> [Char] -> [Char]
Show, (forall x. Rewrite -> Rep Rewrite x)
-> (forall x. Rep Rewrite x -> Rewrite) -> Generic Rewrite
forall x. Rep Rewrite x -> Rewrite
forall x. Rewrite -> Rep Rewrite x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Rewrite -> Rep Rewrite x
from :: forall x. Rewrite -> Rep Rewrite x
$cto :: forall x. Rep Rewrite x -> Rewrite
to :: forall x. Rep Rewrite x -> Rewrite
Generic)
instance Fixpoint AxiomEnv where
toFix :: AxiomEnv -> Doc
toFix AxiomEnv
axe = [Doc] -> Doc
vcat ((Equation -> Doc
forall a. Fixpoint a => a -> Doc
toFix (Equation -> Doc) -> [Equation] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Equation] -> [Equation]
forall a. Ord a => [a] -> [a]
L.sort (AxiomEnv -> [Equation]
aenvEqs AxiomEnv
axe)) [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ (Rewrite -> Doc
forall a. Fixpoint a => a -> Doc
toFix (Rewrite -> Doc) -> [Rewrite] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Rewrite] -> [Rewrite]
forall a. Ord a => [a] -> [a]
L.sort (AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
axe)))
Doc -> Doc -> Doc
$+$ [Doc] -> Doc
forall {a}. Fixpoint a => [a] -> Doc
renderExpand ((Integer, Bool) -> Doc
forall {a} {a}. (Show a, Show a) => (a, a) -> Doc
pairdoc ((Integer, Bool) -> Doc) -> [(Integer, Bool)] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Integer, Bool)] -> [(Integer, Bool)]
forall a. Ord a => [a] -> [a]
L.sort (HashMap Integer Bool -> [(Integer, Bool)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Integer Bool -> [(Integer, Bool)])
-> HashMap Integer Bool -> [(Integer, Bool)]
forall a b. (a -> b) -> a -> b
$ AxiomEnv -> HashMap Integer Bool
aenvExpand AxiomEnv
axe))
Doc -> Doc -> Doc
$+$ HashMap Integer [AutoRewrite] -> Doc
forall a. Fixpoint a => a -> Doc
toFix (AxiomEnv -> HashMap Integer [AutoRewrite]
aenvAutoRW AxiomEnv
axe)
where
pairdoc :: (a, a) -> Doc
pairdoc (a
x,a
y) = [Char] -> Doc
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ a -> [Char]
forall a. Show a => a -> [Char]
show a
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
y
renderExpand :: [a] -> Doc
renderExpand [] = Doc
empty
renderExpand [a]
xs = [Char] -> Doc
text [Char]
"expand" Doc -> Doc -> Doc
<+> [a] -> Doc
forall a. Fixpoint a => a -> Doc
toFix [a]
xs
instance Fixpoint Equation where
toFix :: Equation -> Doc
toFix (Equ Symbol
f [(Symbol, Sort)]
xs Expr
e Sort
s Bool
_) = Doc
"define" Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
f Doc -> Doc -> Doc
<+> [(Symbol, Sort)] -> Doc
forall a. PPrint a => [a] -> Doc
ppArgs [(Symbol, Sort)]
xs Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
s Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"=" Doc -> Doc -> Doc
<+> Doc -> Doc
braces (Doc -> Doc
parens (Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix Expr
e))
instance Fixpoint Rewrite where
toFix :: Rewrite -> Doc
toFix (SMeasure Symbol
f Symbol
d [Symbol]
xs Expr
e)
= [Char] -> Doc
text [Char]
"match"
Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
f
Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
d Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep (Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix (Symbol -> Doc) -> [Symbol] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs)
Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
" = "
Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix Expr
e)
instance PPrint Rewrite where
pprintTidy :: Tidy -> Rewrite -> Doc
pprintTidy Tidy
_ = Rewrite -> Doc
forall a. Fixpoint a => a -> Doc
toFix