{-# LANGUAGE CPP                        #-}
{-# LANGUAGE TupleSections              #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE NoMonomorphismRestriction  #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE ViewPatterns               #-}

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

-- | This module contains the data types, operations and
--   serialization functions for representing Fixpoint's
--   Horn and well-formedness constraints.

module Language.Fixpoint.Types.Sorts (

  -- * Fixpoint Types
    Sort (..)
  , Sub (..)
  , FTycon

  , sortFTycon
  , intFTyCon
  , boolFTyCon
  , realFTyCon
  , numFTyCon
  , strFTyCon
  , setFTyCon
  , mapFTyCon -- TODO: hide these
  , mapFVar
  , basicSorts, intSort, realSort, boolSort, strSort, funcSort
  -- , bitVec32Sort, bitVec64Sort
  , setSort, bitVecSort
  , sizedBitVecSort
  , mapSort, charSort
  , listFTyCon
  , isListTC
  , sizeBv
  , isFirstOrder
  , mappendFTC
  , fTyconSymbol, symbolFTycon, fTyconSort, symbolNumInfoFTyCon
  , fTyconSelfSort
  , fApp
  , fAppTC
  , fObj
  , unFApp
  , unAbs
  , sortAbs

  , mkSortSubst
  , sortSubst
  , functionSort
  , mkFFunc
  , bkFFunc
  , bkAbs
  , mkPoly
  , sortSymbols
  , substSort

  , isNumeric, isReal, isString, isPolyInst

  -- * User-defined ADTs
  , DataField (..)
  , DataCtor (..)
  , DataDecl (..)
  , muSort

  -- * Embedding Source types as Sorts
  , TCEmb, TCArgs (..)
  , tceLookup
  , tceFromList
  , tceToList
  , tceMember
  , tceInsert
  , tceInsertWith
  , tceMap
  ) where

import qualified Data.Store as S
import           Data.Generics             (Data)
import           Data.Typeable             (Typeable)
import           GHC.Generics              (Generic)
import           Data.Hashable
import           Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
import           Data.List                 (foldl')
import           Control.DeepSeq
import           Data.Maybe                (fromMaybe)
import           Language.Fixpoint.Types.Names
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Spans
import           Language.Fixpoint.Misc
import           Text.PrettyPrint.HughesPJ.Compat
import qualified Data.HashMap.Strict       as M
import qualified Data.List                 as L
import qualified Data.Binary as B
import Text.Read (readMaybe)

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

-- instance Show FTycon where
--   show (TC s _) = show (val s)

instance Symbolic FTycon where
  symbol :: FTycon -> Symbol
symbol (TC LocSymbol
s TCInfo
_) = forall a. Symbolic a => a -> Symbol
symbol LocSymbol
s

instance Eq FTycon where
  (TC LocSymbol
s TCInfo
_) == :: FTycon -> FTycon -> Bool
== (TC LocSymbol
s' TCInfo
_) = forall a. Located a -> a
val LocSymbol
s forall a. Eq a => a -> a -> Bool
== forall a. Located a -> a
val LocSymbol
s'

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

mappendFTC :: FTycon -> FTycon -> FTycon
mappendFTC :: FTycon -> FTycon -> FTycon
mappendFTC (TC LocSymbol
x TCInfo
i1) (TC LocSymbol
_ TCInfo
i2) = LocSymbol -> TCInfo -> FTycon
TC LocSymbol
x (forall a. Monoid a => a -> a -> a
mappend TCInfo
i1 TCInfo
i2)

instance Semigroup TCInfo where
 TCInfo Bool
i1 Bool
i2 Bool
i3 <> :: TCInfo -> TCInfo -> TCInfo
<> TCInfo Bool
i1' Bool
i2' Bool
i3' = Bool -> Bool -> Bool -> TCInfo
TCInfo (Bool
i1 Bool -> Bool -> Bool
|| Bool
i1') (Bool
i2 Bool -> Bool -> Bool
|| Bool
i2') (Bool
i3 Bool -> Bool -> Bool
|| Bool
i3')

instance Monoid TCInfo where
  mempty :: TCInfo
mempty  = Bool -> Bool -> Bool -> TCInfo
TCInfo Bool
defNumInfo Bool
defRealInfo Bool
defStrInfo
  mappend :: TCInfo -> TCInfo -> TCInfo
mappend = forall a. Semigroup a => a -> a -> a
(<>)

defTcInfo, numTcInfo, realTcInfo, strTcInfo :: TCInfo
defTcInfo :: TCInfo
defTcInfo  = Bool -> Bool -> Bool -> TCInfo
TCInfo Bool
defNumInfo Bool
defRealInfo Bool
defStrInfo
numTcInfo :: TCInfo
numTcInfo  = Bool -> Bool -> Bool -> TCInfo
TCInfo Bool
True       Bool
defRealInfo Bool
defStrInfo
realTcInfo :: TCInfo
realTcInfo = Bool -> Bool -> Bool -> TCInfo
TCInfo Bool
True       Bool
True        Bool
defStrInfo
strTcInfo :: TCInfo
strTcInfo  = Bool -> Bool -> Bool -> TCInfo
TCInfo Bool
defNumInfo Bool
defRealInfo Bool
True

defNumInfo, defRealInfo, defStrInfo :: Bool
defNumInfo :: Bool
defNumInfo  = Bool
False
defRealInfo :: Bool
defRealInfo = Bool
False
defStrInfo :: Bool
defStrInfo  = Bool
False

charFTyCon, intFTyCon, boolFTyCon, realFTyCon, funcFTyCon, numFTyCon :: FTycon
strFTyCon, listFTyCon, mapFTyCon, setFTyCon :: FTycon
intFTyCon :: FTycon
intFTyCon  = LocSymbol -> TCInfo -> FTycon
TC (forall a. a -> Located a
dummyLoc Symbol
"int"      ) TCInfo
numTcInfo
boolFTyCon :: FTycon
boolFTyCon = LocSymbol -> TCInfo -> FTycon
TC (forall a. a -> Located a
dummyLoc Symbol
"bool"     ) TCInfo
defTcInfo
realFTyCon :: FTycon
realFTyCon = LocSymbol -> TCInfo -> FTycon
TC (forall a. a -> Located a
dummyLoc Symbol
"real"     ) TCInfo
realTcInfo
numFTyCon :: FTycon
numFTyCon  = LocSymbol -> TCInfo -> FTycon
TC (forall a. a -> Located a
dummyLoc Symbol
"num"      ) TCInfo
numTcInfo
funcFTyCon :: FTycon
funcFTyCon = LocSymbol -> TCInfo -> FTycon
TC (forall a. a -> Located a
dummyLoc Symbol
"function" ) TCInfo
defTcInfo
strFTyCon :: FTycon
strFTyCon  = LocSymbol -> TCInfo -> FTycon
TC (forall a. a -> Located a
dummyLoc forall a. IsString a => a
strConName ) TCInfo
strTcInfo
listFTyCon :: FTycon
listFTyCon = LocSymbol -> TCInfo -> FTycon
TC (forall a. a -> Located a
dummyLoc Symbol
listConName) TCInfo
defTcInfo
charFTyCon :: FTycon
charFTyCon = LocSymbol -> TCInfo -> FTycon
TC (forall a. a -> Located a
dummyLoc forall a. IsString a => a
charConName) TCInfo
defTcInfo
setFTyCon :: FTycon
setFTyCon  = LocSymbol -> TCInfo -> FTycon
TC (forall a. a -> Located a
dummyLoc Symbol
setConName ) TCInfo
defTcInfo
mapFTyCon :: FTycon
mapFTyCon  = LocSymbol -> TCInfo -> FTycon
TC (forall a. a -> Located a
dummyLoc Symbol
mapConName ) TCInfo
defTcInfo

isListConName :: LocSymbol -> Bool
isListConName :: LocSymbol -> Bool
isListConName LocSymbol
x = Symbol
c forall a. Eq a => a -> a -> Bool
== Symbol
listConName Bool -> Bool -> Bool
|| Symbol
c forall a. Eq a => a -> a -> Bool
== Symbol
listLConName --"List"
  where
    c :: Symbol
c           = forall a. Located a -> a
val LocSymbol
x

isListTC :: FTycon -> Bool
isListTC :: FTycon -> Bool
isListTC (TC LocSymbol
z TCInfo
_) = LocSymbol -> Bool
isListConName LocSymbol
z

sizeBv :: FTycon -> Maybe Int
sizeBv :: FTycon -> Maybe Int
sizeBv FTycon
tc = do
  let s :: Symbol
s = forall a. Located a -> a
val forall a b. (a -> b) -> a -> b
$ FTycon -> LocSymbol
fTyconSymbol FTycon
tc
  Symbol
size <- Symbol -> Symbol -> Maybe Symbol
stripPrefix Symbol
sizeName Symbol
s
  forall a. Read a => String -> Maybe a
readMaybe forall a b. (a -> b) -> a -> b
$ Symbol -> String
symbolString Symbol
size

fTyconSymbol :: FTycon -> Located Symbol
fTyconSymbol :: FTycon -> LocSymbol
fTyconSymbol (TC LocSymbol
s TCInfo
_) = LocSymbol
s

symbolNumInfoFTyCon :: LocSymbol -> Bool -> Bool -> FTycon
symbolNumInfoFTyCon :: LocSymbol -> Bool -> Bool -> FTycon
symbolNumInfoFTyCon LocSymbol
c Bool
isNum Bool
isReal
  | LocSymbol -> Bool
isListConName LocSymbol
c
  = LocSymbol -> TCInfo -> FTycon
TC (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. a -> b -> a
const Symbol
listConName) LocSymbol
c) TCInfo
tcinfo
  | Bool
otherwise
  = LocSymbol -> TCInfo -> FTycon
TC LocSymbol
c TCInfo
tcinfo
  where
    tcinfo :: TCInfo
tcinfo = TCInfo
defTcInfo { tc_isNum :: Bool
tc_isNum = Bool
isNum, tc_isReal :: Bool
tc_isReal = Bool
isReal}



symbolFTycon :: LocSymbol -> FTycon
symbolFTycon :: LocSymbol -> FTycon
symbolFTycon LocSymbol
c = LocSymbol -> Bool -> Bool -> FTycon
symbolNumInfoFTyCon LocSymbol
c Bool
defNumInfo Bool
defRealInfo

fApp :: Sort -> [Sort] -> Sort
fApp :: Sort -> [Sort] -> Sort
fApp = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Sort -> Sort -> Sort
FApp

fAppTC :: FTycon -> [Sort] -> Sort
fAppTC :: FTycon -> [Sort] -> Sort
fAppTC = Sort -> [Sort] -> Sort
fApp forall b c a. (b -> c) -> (a -> b) -> a -> c
. FTycon -> Sort
fTyconSort

fTyconSelfSort :: FTycon -> Int -> Sort
fTyconSelfSort :: FTycon -> Int -> Sort
fTyconSelfSort FTycon
c Int
n = FTycon -> [Sort] -> Sort
fAppTC FTycon
c [Int -> Sort
FVar Int
i | Int
i <- [Int
0..(Int
n forall a. Num a => a -> a -> a
- Int
1)]]

-- | fApp' (FApp (FApp "Map" key) val) ===> ["Map", key, val]
--   That is, `fApp'` is used to split a type application into
--   the FTyCon and its args.

unFApp :: Sort -> ListNE Sort
unFApp :: Sort -> [Sort]
unFApp = [Sort] -> Sort -> [Sort]
go []
  where
    go :: [Sort] -> Sort -> [Sort]
go [Sort]
acc (FApp Sort
t1 Sort
t2) = [Sort] -> Sort -> [Sort]
go (Sort
t2 forall a. a -> [a] -> [a]
: [Sort]
acc) Sort
t1
    go [Sort]
acc Sort
t            = Sort
t forall a. a -> [a] -> [a]
: [Sort]
acc

unAbs :: Sort -> Sort
unAbs :: Sort -> Sort
unAbs (FAbs Int
_ Sort
s) = Sort -> Sort
unAbs Sort
s
unAbs Sort
s          = Sort
s

fObj :: LocSymbol -> Sort
fObj :: LocSymbol -> Sort
fObj = FTycon -> Sort
fTyconSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocSymbol -> TCInfo -> FTycon
`TC` TCInfo
defTcInfo)

sortFTycon :: Sort -> Maybe FTycon
sortFTycon :: Sort -> Maybe FTycon
sortFTycon Sort
FInt    = forall a. a -> Maybe a
Just FTycon
intFTyCon
sortFTycon Sort
FReal   = forall a. a -> Maybe a
Just FTycon
realFTyCon
sortFTycon Sort
FNum    = forall a. a -> Maybe a
Just FTycon
numFTyCon
sortFTycon (FTC FTycon
c) = forall a. a -> Maybe a
Just FTycon
c
sortFTycon Sort
_       = forall a. Maybe a
Nothing


functionSort :: Sort -> Maybe ([Int], [Sort], Sort)
functionSort :: Sort -> Maybe ([Int], [Sort], Sort)
functionSort Sort
s
  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
is Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Sort]
ss
  = forall a. Maybe a
Nothing
  | Bool
otherwise
  = forall a. a -> Maybe a
Just ([Int]
is, [Sort]
ss, Sort
r)
  where
    ([Int]
is, [Sort]
ss, Sort
r)            = [Int] -> [Sort] -> Sort -> ([Int], [Sort], Sort)
go [] [] Sort
s
    go :: [Int] -> [Sort] -> Sort -> ([Int], [Sort], Sort)
go [Int]
vs [Sort]
ss (FAbs Int
i Sort
t)    = [Int] -> [Sort] -> Sort -> ([Int], [Sort], Sort)
go (Int
iforall a. a -> [a] -> [a]
:[Int]
vs) [Sort]
ss Sort
t
    go [Int]
vs [Sort]
ss (FFunc Sort
s1 Sort
s2) = [Int] -> [Sort] -> Sort -> ([Int], [Sort], Sort)
go [Int]
vs (Sort
s1forall a. a -> [a] -> [a]
:[Sort]
ss) Sort
s2
    go [Int]
vs [Sort]
ss Sort
t             = (forall a. [a] -> [a]
reverse [Int]
vs, forall a. [a] -> [a]
reverse [Sort]
ss, Sort
t)


sortAbs :: Sort -> Int
sortAbs :: Sort -> Int
sortAbs (FAbs Int
i Sort
s)    = forall a. Ord a => a -> a -> a
max Int
i (Sort -> Int
sortAbs Sort
s)
sortAbs (FFunc Sort
s1 Sort
s2) = forall a. Ord a => a -> a -> a
max (Sort -> Int
sortAbs Sort
s1) (Sort -> Int
sortAbs Sort
s2)
sortAbs (FApp  Sort
s1 Sort
s2) = forall a. Ord a => a -> a -> a
max (Sort -> Int
sortAbs Sort
s1) (Sort -> Int
sortAbs Sort
s2)
sortAbs Sort
_             = -Int
1

mapFVar :: (Int -> Int) -> Sort -> Sort
mapFVar :: (Int -> Int) -> Sort -> Sort
mapFVar Int -> Int
f = Sort -> Sort
go
  where go :: Sort -> Sort
go (FVar Int
i)      = Int -> Sort
FVar (Int -> Int
f Int
i)
        go (FAbs Int
i Sort
t)    = Int -> Sort -> Sort
FAbs (Int -> Int
f Int
i) (Sort -> Sort
go Sort
t)
        go (FFunc Sort
t1 Sort
t2) = Sort -> Sort -> Sort
FFunc (Sort -> Sort
go Sort
t1) (Sort -> Sort
go Sort
t2)
        go (FApp Sort
t1 Sort
t2)  = Sort -> Sort -> Sort
FApp (Sort -> Sort
go Sort
t1) (Sort -> Sort
go Sort
t2)
        go t :: Sort
t@(FObj Symbol
_)    = Sort
t
        go t :: Sort
t@(FTC FTycon
_)     = Sort
t
        go t :: Sort
t@Sort
FInt        = Sort
t
        go t :: Sort
t@Sort
FReal       = Sort
t
        go t :: Sort
t@Sort
FNum        = Sort
t
        go t :: Sort
t@Sort
FFrac       = Sort
t

--------------------------------------------------------------------------------
-- | Sorts ---------------------------------------------------------------------
--------------------------------------------------------------------------------
data Sort = FInt
          | FReal
          | FNum                 -- ^ numeric kind for Num tyvars
          | FFrac                -- ^ numeric kind for Fractional tyvars
          | FObj  !Symbol        -- ^ uninterpreted type
          | FVar  !Int           -- ^ fixpoint type variable
          | FFunc !Sort !Sort    -- ^ function
          | FAbs  !Int !Sort     -- ^ type-abstraction
          | FTC   !FTycon
          | FApp  !Sort !Sort    -- ^ constructed type
            deriving (Sort -> Sort -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sort -> Sort -> Bool
$c/= :: Sort -> Sort -> Bool
== :: Sort -> Sort -> Bool
$c== :: Sort -> Sort -> Bool
Eq, Eq Sort
Sort -> Sort -> Bool
Sort -> Sort -> Ordering
Sort -> Sort -> Sort
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
min :: Sort -> Sort -> Sort
$cmin :: Sort -> Sort -> Sort
max :: Sort -> Sort -> Sort
$cmax :: Sort -> Sort -> Sort
>= :: Sort -> Sort -> Bool
$c>= :: Sort -> Sort -> Bool
> :: Sort -> Sort -> Bool
$c> :: Sort -> Sort -> Bool
<= :: Sort -> Sort -> Bool
$c<= :: Sort -> Sort -> Bool
< :: Sort -> Sort -> Bool
$c< :: Sort -> Sort -> Bool
compare :: Sort -> Sort -> Ordering
$ccompare :: Sort -> Sort -> Ordering
Ord, Int -> Sort -> ShowS
[Sort] -> ShowS
Sort -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sort] -> ShowS
$cshowList :: [Sort] -> ShowS
show :: Sort -> String
$cshow :: Sort -> String
showsPrec :: Int -> Sort -> ShowS
$cshowsPrec :: Int -> Sort -> ShowS
Show, Typeable Sort
Sort -> DataType
Sort -> Constr
(forall b. Data b => b -> b) -> Sort -> Sort
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) -> Sort -> u
forall u. (forall d. Data d => d -> u) -> Sort -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sort
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sort -> c Sort
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sort)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sort)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sort -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sort -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Sort -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Sort -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r
gmapT :: (forall b. Data b => b -> b) -> Sort -> Sort
$cgmapT :: (forall b. Data b => b -> b) -> Sort -> Sort
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sort)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sort)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sort)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sort)
dataTypeOf :: Sort -> DataType
$cdataTypeOf :: Sort -> DataType
toConstr :: Sort -> Constr
$ctoConstr :: Sort -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sort
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sort
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sort -> c Sort
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sort -> c Sort
Data, Typeable, forall x. Rep Sort x -> Sort
forall x. Sort -> Rep Sort x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Sort x -> Sort
$cfrom :: forall x. Sort -> Rep Sort x
Generic)

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

sortSymbols :: Sort -> HashSet Symbol
sortSymbols :: Sort -> HashSet Symbol
sortSymbols = \case
  FObj Symbol
s -> forall a. Hashable a => a -> HashSet a
HashSet.singleton Symbol
s
  FFunc Sort
t0 Sort
t1 -> forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union (Sort -> HashSet Symbol
sortSymbols Sort
t0) (Sort -> HashSet Symbol
sortSymbols Sort
t1)
  FAbs Int
_ Sort
t -> Sort -> HashSet Symbol
sortSymbols Sort
t
  FApp Sort
t0 Sort
t1 -> forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union (Sort -> HashSet Symbol
sortSymbols Sort
t0) (Sort -> HashSet Symbol
sortSymbols Sort
t1)
  Sort
_ -> forall a. HashSet a
HashSet.empty

substSort :: (Symbol -> Sort) -> Sort -> Sort
substSort :: (Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f = \case
  FObj Symbol
s -> Symbol -> Sort
f Symbol
s
  FFunc Sort
t0 Sort
t1 -> Sort -> Sort -> Sort
FFunc ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f Sort
t0) ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f Sort
t1)
  FApp Sort
t0 Sort
t1 -> Sort -> Sort -> Sort
FApp ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f Sort
t0) ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f Sort
t1)
  FAbs Int
i Sort
t -> Int -> Sort -> Sort
FAbs Int
i ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f Sort
t)
  Sort
t -> Sort
t

data DataField = DField
  { DataField -> LocSymbol
dfName :: !LocSymbol          -- ^ Field Name
  , DataField -> Sort
dfSort :: !Sort               -- ^ Field Sort
  } deriving (DataField -> DataField -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DataField -> DataField -> Bool
$c/= :: DataField -> DataField -> Bool
== :: DataField -> DataField -> Bool
$c== :: DataField -> DataField -> Bool
Eq, Eq DataField
DataField -> DataField -> Bool
DataField -> DataField -> Ordering
DataField -> DataField -> DataField
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
min :: DataField -> DataField -> DataField
$cmin :: DataField -> DataField -> DataField
max :: DataField -> DataField -> DataField
$cmax :: DataField -> DataField -> DataField
>= :: DataField -> DataField -> Bool
$c>= :: DataField -> DataField -> Bool
> :: DataField -> DataField -> Bool
$c> :: DataField -> DataField -> Bool
<= :: DataField -> DataField -> Bool
$c<= :: DataField -> DataField -> Bool
< :: DataField -> DataField -> Bool
$c< :: DataField -> DataField -> Bool
compare :: DataField -> DataField -> Ordering
$ccompare :: DataField -> DataField -> Ordering
Ord, Int -> DataField -> ShowS
[DataField] -> ShowS
DataField -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DataField] -> ShowS
$cshowList :: [DataField] -> ShowS
show :: DataField -> String
$cshow :: DataField -> String
showsPrec :: Int -> DataField -> ShowS
$cshowsPrec :: Int -> DataField -> ShowS
Show, Typeable DataField
DataField -> DataType
DataField -> Constr
(forall b. Data b => b -> b) -> DataField -> DataField
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) -> DataField -> u
forall u. (forall d. Data d => d -> u) -> DataField -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataField -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataField -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataField
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataField -> c DataField
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataField)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataField)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataField -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataField -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> DataField -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DataField -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataField -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataField -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataField -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataField -> r
gmapT :: (forall b. Data b => b -> b) -> DataField -> DataField
$cgmapT :: (forall b. Data b => b -> b) -> DataField -> DataField
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataField)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataField)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataField)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataField)
dataTypeOf :: DataField -> DataType
$cdataTypeOf :: DataField -> DataType
toConstr :: DataField -> Constr
$ctoConstr :: DataField -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataField
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataField
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataField -> c DataField
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataField -> c DataField
Data, Typeable, forall x. Rep DataField x -> DataField
forall x. DataField -> Rep DataField x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DataField x -> DataField
$cfrom :: forall x. DataField -> Rep DataField x
Generic)

data DataCtor = DCtor
  { DataCtor -> LocSymbol
dcName   :: !LocSymbol        -- ^ Ctor Name
  , DataCtor -> [DataField]
dcFields :: ![DataField]      -- ^ Ctor Fields
  } deriving (DataCtor -> DataCtor -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DataCtor -> DataCtor -> Bool
$c/= :: DataCtor -> DataCtor -> Bool
== :: DataCtor -> DataCtor -> Bool
$c== :: DataCtor -> DataCtor -> Bool
Eq, Eq DataCtor
DataCtor -> DataCtor -> Bool
DataCtor -> DataCtor -> Ordering
DataCtor -> DataCtor -> DataCtor
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
min :: DataCtor -> DataCtor -> DataCtor
$cmin :: DataCtor -> DataCtor -> DataCtor
max :: DataCtor -> DataCtor -> DataCtor
$cmax :: DataCtor -> DataCtor -> DataCtor
>= :: DataCtor -> DataCtor -> Bool
$c>= :: DataCtor -> DataCtor -> Bool
> :: DataCtor -> DataCtor -> Bool
$c> :: DataCtor -> DataCtor -> Bool
<= :: DataCtor -> DataCtor -> Bool
$c<= :: DataCtor -> DataCtor -> Bool
< :: DataCtor -> DataCtor -> Bool
$c< :: DataCtor -> DataCtor -> Bool
compare :: DataCtor -> DataCtor -> Ordering
$ccompare :: DataCtor -> DataCtor -> Ordering
Ord, Int -> DataCtor -> ShowS
[DataCtor] -> ShowS
DataCtor -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DataCtor] -> ShowS
$cshowList :: [DataCtor] -> ShowS
show :: DataCtor -> String
$cshow :: DataCtor -> String
showsPrec :: Int -> DataCtor -> ShowS
$cshowsPrec :: Int -> DataCtor -> ShowS
Show, Typeable DataCtor
DataCtor -> DataType
DataCtor -> Constr
(forall b. Data b => b -> b) -> DataCtor -> DataCtor
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) -> DataCtor -> u
forall u. (forall d. Data d => d -> u) -> DataCtor -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataCtor -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataCtor -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataCtor -> m DataCtor
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataCtor -> m DataCtor
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataCtor
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataCtor -> c DataCtor
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataCtor)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataCtor)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataCtor -> m DataCtor
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataCtor -> m DataCtor
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataCtor -> m DataCtor
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataCtor -> m DataCtor
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataCtor -> m DataCtor
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataCtor -> m DataCtor
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataCtor -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataCtor -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> DataCtor -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DataCtor -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataCtor -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataCtor -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataCtor -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataCtor -> r
gmapT :: (forall b. Data b => b -> b) -> DataCtor -> DataCtor
$cgmapT :: (forall b. Data b => b -> b) -> DataCtor -> DataCtor
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataCtor)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataCtor)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataCtor)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataCtor)
dataTypeOf :: DataCtor -> DataType
$cdataTypeOf :: DataCtor -> DataType
toConstr :: DataCtor -> Constr
$ctoConstr :: DataCtor -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataCtor
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataCtor
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataCtor -> c DataCtor
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataCtor -> c DataCtor
Data, Typeable, forall x. Rep DataCtor x -> DataCtor
forall x. DataCtor -> Rep DataCtor x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DataCtor x -> DataCtor
$cfrom :: forall x. DataCtor -> Rep DataCtor x
Generic)

data DataDecl = DDecl
  { DataDecl -> FTycon
ddTyCon :: !FTycon            -- ^ Name of defined datatype
  , DataDecl -> Int
ddVars  :: !Int               -- ^ Number of type variables
  , DataDecl -> [DataCtor]
ddCtors :: [DataCtor]         -- ^ Datatype Ctors. Invariant: type variables bound in ctors are greater than ddVars
  } deriving (DataDecl -> DataDecl -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DataDecl -> DataDecl -> Bool
$c/= :: DataDecl -> DataDecl -> Bool
== :: DataDecl -> DataDecl -> Bool
$c== :: DataDecl -> DataDecl -> Bool
Eq, Eq DataDecl
DataDecl -> DataDecl -> Bool
DataDecl -> DataDecl -> Ordering
DataDecl -> DataDecl -> DataDecl
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
min :: DataDecl -> DataDecl -> DataDecl
$cmin :: DataDecl -> DataDecl -> DataDecl
max :: DataDecl -> DataDecl -> DataDecl
$cmax :: DataDecl -> DataDecl -> DataDecl
>= :: DataDecl -> DataDecl -> Bool
$c>= :: DataDecl -> DataDecl -> Bool
> :: DataDecl -> DataDecl -> Bool
$c> :: DataDecl -> DataDecl -> Bool
<= :: DataDecl -> DataDecl -> Bool
$c<= :: DataDecl -> DataDecl -> Bool
< :: DataDecl -> DataDecl -> Bool
$c< :: DataDecl -> DataDecl -> Bool
compare :: DataDecl -> DataDecl -> Ordering
$ccompare :: DataDecl -> DataDecl -> Ordering
Ord, Int -> DataDecl -> ShowS
[DataDecl] -> ShowS
DataDecl -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DataDecl] -> ShowS
$cshowList :: [DataDecl] -> ShowS
show :: DataDecl -> String
$cshow :: DataDecl -> String
showsPrec :: Int -> DataDecl -> ShowS
$cshowsPrec :: Int -> DataDecl -> ShowS
Show, Typeable DataDecl
DataDecl -> DataType
DataDecl -> Constr
(forall b. Data b => b -> b) -> DataDecl -> DataDecl
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) -> DataDecl -> u
forall u. (forall d. Data d => d -> u) -> DataDecl -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataDecl -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataDecl -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataDecl -> m DataDecl
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataDecl -> m DataDecl
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataDecl
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataDecl -> c DataDecl
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataDecl)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataDecl)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataDecl -> m DataDecl
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataDecl -> m DataDecl
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataDecl -> m DataDecl
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataDecl -> m DataDecl
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataDecl -> m DataDecl
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataDecl -> m DataDecl
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataDecl -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataDecl -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> DataDecl -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DataDecl -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataDecl -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataDecl -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataDecl -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataDecl -> r
gmapT :: (forall b. Data b => b -> b) -> DataDecl -> DataDecl
$cgmapT :: (forall b. Data b => b -> b) -> DataDecl -> DataDecl
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataDecl)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataDecl)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataDecl)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataDecl)
dataTypeOf :: DataDecl -> DataType
$cdataTypeOf :: DataDecl -> DataType
toConstr :: DataDecl -> Constr
$ctoConstr :: DataDecl -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataDecl
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataDecl
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataDecl -> c DataDecl
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataDecl -> c DataDecl
Data, Typeable, forall x. Rep DataDecl x -> DataDecl
forall x. DataDecl -> Rep DataDecl x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DataDecl x -> DataDecl
$cfrom :: forall x. DataDecl -> Rep DataDecl x
Generic)

instance Loc DataDecl where
    srcSpan :: DataDecl -> SrcSpan
srcSpan (DDecl FTycon
ty Int
_ [DataCtor]
_) = forall a. Loc a => a -> SrcSpan
srcSpan FTycon
ty

instance Symbolic DataDecl where
  symbol :: DataDecl -> Symbol
symbol = forall a. Symbolic a => a -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDecl -> FTycon
ddTyCon

instance Symbolic DataField where
  symbol :: DataField -> Symbol
symbol = forall a. Located a -> a
val forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataField -> LocSymbol
dfName

instance Symbolic DataCtor where
  symbol :: DataCtor -> Symbol
symbol = forall a. Located a -> a
val forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCtor -> LocSymbol
dcName

--------------------------------------------------------------------------------------------------
muSort  :: [DataDecl] -> [DataDecl]
muSort :: [DataDecl] -> [DataDecl]
muSort [DataDecl]
dds = (Sort -> Sort) -> DataDecl -> DataDecl
mapSortDataDecl Sort -> Sort
tx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataDecl]
dds
  where
    selfs :: [(Sort, Sort)]
selfs = [(FTycon -> Int -> Sort
fTyconSelfSort FTycon
c Int
n, FTycon -> Sort
fTyconSort FTycon
c) | DDecl FTycon
c Int
n [DataCtor]
_ <- [DataDecl]
dds]
    tx :: Sort -> Sort
tx Sort
t  = forall a. a -> Maybe a -> a
fromMaybe Sort
t forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Sort
t [(Sort, Sort)]
selfs

    mapSortDataDecl :: (Sort -> Sort) -> DataDecl -> DataDecl
mapSortDataDecl Sort -> Sort
f  DataDecl
dd = DataDecl
dd { ddCtors :: [DataCtor]
ddCtors  = (Sort -> Sort) -> DataCtor -> DataCtor
mapSortDataCTor Sort -> Sort
f  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataDecl -> [DataCtor]
ddCtors  DataDecl
dd }
    mapSortDataCTor :: (Sort -> Sort) -> DataCtor -> DataCtor
mapSortDataCTor Sort -> Sort
f  DataCtor
ct = DataCtor
ct { dcFields :: [DataField]
dcFields = (Sort -> Sort) -> DataField -> DataField
mapSortDataField Sort -> Sort
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCtor -> [DataField]
dcFields DataCtor
ct }
    mapSortDataField :: (Sort -> Sort) -> DataField -> DataField
mapSortDataField Sort -> Sort
f DataField
df = DataField
df { dfSort :: Sort
dfSort   = Sort -> Sort
f forall a b. (a -> b) -> a -> b
$ DataField -> Sort
dfSort DataField
df }


isFirstOrder, isFunction :: Sort -> Bool
isFirstOrder :: Sort -> Bool
isFirstOrder (FFunc Sort
sx Sort
s) = Bool -> Bool
not (Sort -> Bool
isFunction Sort
sx) Bool -> Bool -> Bool
&& Sort -> Bool
isFirstOrder Sort
s
isFirstOrder (FAbs Int
_ Sort
s)   = Sort -> Bool
isFirstOrder Sort
s
isFirstOrder (FApp Sort
s1 Sort
s2) = Bool -> Bool
not (Sort -> Bool
isFunction Sort
s1) Bool -> Bool -> Bool
&& Bool -> Bool
not (Sort -> Bool
isFunction Sort
s2)
isFirstOrder Sort
_            = Bool
True

isFunction :: Sort -> Bool
isFunction (FAbs Int
_ Sort
s)  = Sort -> Bool
isFunction Sort
s
isFunction (FFunc Sort
_ Sort
_) = Bool
True
isFunction Sort
_           = Bool
False

isNumeric :: Sort -> Bool
isNumeric :: Sort -> Bool
isNumeric Sort
FInt           = Bool
True
isNumeric Sort
FReal          = Bool
True
isNumeric (FApp Sort
s Sort
_)     = Sort -> Bool
isNumeric Sort
s
isNumeric (FTC (TC LocSymbol
_ TCInfo
i)) = TCInfo -> Bool
tc_isNum TCInfo
i
isNumeric (FAbs Int
_ Sort
s)     = Sort -> Bool
isNumeric Sort
s
isNumeric Sort
_              = Bool
False

isReal :: Sort -> Bool
isReal :: Sort -> Bool
isReal Sort
FReal          = Bool
True
isReal (FApp Sort
s Sort
_)     = Sort -> Bool
isReal Sort
s
isReal (FTC (TC LocSymbol
_ TCInfo
i)) = TCInfo -> Bool
tc_isReal TCInfo
i
isReal (FAbs Int
_ Sort
s)     = Sort -> Bool
isReal Sort
s
isReal Sort
_              = Bool
False


isString :: Sort -> Bool
isString :: Sort -> Bool
isString (FApp Sort
l Sort
c)     = (Sort -> Bool
isList Sort
l Bool -> Bool -> Bool
&& Sort -> Bool
isChar Sort
c) Bool -> Bool -> Bool
|| Sort -> Bool
isString Sort
l
isString (FTC (TC LocSymbol
c TCInfo
i)) = forall a. Located a -> a
val LocSymbol
c forall a. Eq a => a -> a -> Bool
== forall a. IsString a => a
strConName Bool -> Bool -> Bool
|| TCInfo -> Bool
tc_isString TCInfo
i
isString (FAbs Int
_ Sort
s)     = Sort -> Bool
isString Sort
s
isString Sort
_              = Bool
False

isList :: Sort -> Bool
isList :: Sort -> Bool
isList (FTC FTycon
c) = FTycon -> Bool
isListTC FTycon
c
isList Sort
_       = Bool
False

isChar :: Sort -> Bool
isChar :: Sort -> Bool
isChar (FTC FTycon
c) = FTycon
c forall a. Eq a => a -> a -> Bool
== FTycon
charFTyCon
isChar Sort
_       = Bool
False

{-@ FFunc :: Nat -> ListNE Sort -> Sort @-}

mkFFunc :: Int -> [Sort] -> Sort
mkFFunc :: Int -> [Sort] -> Sort
mkFFunc Int
i [Sort]
ss     = [Int] -> [Sort] -> Sort
go [Int
0..Int
iforall a. Num a => a -> a -> a
-Int
1] [Sort]
ss
  where
    go :: [Int] -> [Sort] -> Sort
go [] [Sort
s]    = Sort
s
    go [] (Sort
s:[Sort]
ss) = Sort -> Sort -> Sort
FFunc Sort
s forall a b. (a -> b) -> a -> b
$ [Int] -> [Sort] -> Sort
go [] [Sort]
ss
    go (Int
i:[Int]
is) [Sort]
ss = Int -> Sort -> Sort
FAbs  Int
i forall a b. (a -> b) -> a -> b
$ [Int] -> [Sort] -> Sort
go [Int]
is [Sort]
ss
    go [Int]
_ [Sort]
_       = forall a. HasCallStack => String -> a
error String
"cannot happen"

   -- foldl' (flip FAbs) (foldl1 (flip FFunc) ss) [0..i-1]

bkFFunc :: Sort -> Maybe (Int, [Sort])
bkFFunc :: Sort -> Maybe (Int, [Sort])
bkFFunc Sort
t    = (forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 forall a. a -> [a] -> [a]
: [Int]
as),) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> Maybe [Sort]
bkFun Sort
t'
  where
    ([Int]
as, Sort
t') = Sort -> ([Int], Sort)
bkAbs Sort
t

bkAbs :: Sort -> ([Int], Sort)
bkAbs :: Sort -> ([Int], Sort)
bkAbs (FAbs Int
i Sort
t) = (Int
iforall a. a -> [a] -> [a]
:[Int]
is, Sort
t') where ([Int]
is, Sort
t') = Sort -> ([Int], Sort)
bkAbs Sort
t
bkAbs Sort
t          = ([], Sort
t)

bkFun :: Sort -> Maybe [Sort]
bkFun :: Sort -> Maybe [Sort]
bkFun z :: Sort
z@(FFunc Sort
_ Sort
_)  = forall a. a -> Maybe a
Just (Sort -> [Sort]
go Sort
z)
  where
    go :: Sort -> [Sort]
go (FFunc Sort
t1 Sort
t2) = Sort
t1 forall a. a -> [a] -> [a]
: Sort -> [Sort]
go Sort
t2
    go Sort
t             = [Sort
t]
bkFun Sort
_              = forall a. Maybe a
Nothing

isPolyInst :: Sort -> Sort -> Bool
isPolyInst :: Sort -> Sort -> Bool
isPolyInst Sort
s Sort
t = Sort -> Bool
isPoly Sort
s Bool -> Bool -> Bool
&& Bool -> Bool
not (Sort -> Bool
isPoly Sort
t)

isPoly :: Sort -> Bool
isPoly :: Sort -> Bool
isPoly FAbs {} = Bool
True
isPoly Sort
_       = Bool
False

mkPoly :: Int -> Sort -> Sort
mkPoly :: Int -> Sort -> Sort
mkPoly Int
i Sort
s = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Sort -> Sort
FAbs) Sort
s [Int
0..Int
i]


instance Hashable FTycon where
  hashWithSalt :: Int -> FTycon -> Int
hashWithSalt Int
i (TC LocSymbol
s TCInfo
_) = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
i LocSymbol
s

instance Loc FTycon where
  srcSpan :: FTycon -> SrcSpan
srcSpan (TC LocSymbol
c TCInfo
_) = forall a. Loc a => a -> SrcSpan
srcSpan LocSymbol
c

instance Hashable Sort

newtype Sub = Sub [(Int, Sort)] deriving (forall x. Rep Sub x -> Sub
forall x. Sub -> Rep Sub x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Sub x -> Sub
$cfrom :: forall x. Sub -> Rep Sub x
Generic)

instance Fixpoint Sort where
  toFix :: Sort -> Doc
toFix = Sort -> Doc
toFixSort

toFixSort :: Sort -> Doc
toFixSort :: Sort -> Doc
toFixSort (FVar Int
i)     = String -> Doc
text String
"@" Doc -> Doc -> Doc
<-> Doc -> Doc
parens (forall a. Fixpoint a => a -> Doc
toFix Int
i)
toFixSort Sort
FInt         = String -> Doc
text String
"int"
toFixSort Sort
FReal        = String -> Doc
text String
"real"
toFixSort Sort
FFrac        = String -> Doc
text String
"frac"
toFixSort (FObj Symbol
x)     = forall a. Fixpoint a => a -> Doc
toFix Symbol
x
toFixSort Sort
FNum         = String -> Doc
text String
"num"
toFixSort t :: Sort
t@(FAbs Int
_ Sort
_) = Sort -> Doc
toFixAbsApp Sort
t
toFixSort t :: Sort
t@(FFunc Sort
_ Sort
_)= Sort -> Doc
toFixAbsApp Sort
t
toFixSort (FTC FTycon
c)      = forall a. Fixpoint a => a -> Doc
toFix FTycon
c
toFixSort t :: Sort
t@(FApp Sort
_ Sort
_) = [Sort] -> Doc
toFixFApp (Sort -> [Sort]
unFApp Sort
t)

toFixAbsApp :: Sort -> Doc
toFixAbsApp :: Sort -> Doc
toFixAbsApp (Sort -> Maybe ([Int], [Sort], Sort)
functionSort -> Just ([Int]
vs, [Sort]
ss, Sort
s)) =
  String -> Doc
text String
"func" Doc -> Doc -> Doc
<-> Doc -> Doc
parens (forall a. Fixpoint a => a -> Doc
toFix Int
n Doc -> Doc -> Doc
<+> String -> Doc
text String
"," Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix [Sort]
ts)
  where
    n :: Int
n                = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
vs
    ts :: [Sort]
ts               = [Sort]
ss forall a. [a] -> [a] -> [a]
++ [Sort
s]
toFixAbsApp Sort
_ = forall a. HasCallStack => String -> a
error String
"Unexpected nothing function sort"

toFixFApp            :: ListNE Sort -> Doc
toFixFApp :: [Sort] -> Doc
toFixFApp [Sort
t]        = Sort -> Doc
toFixSort Sort
t
toFixFApp [FTC FTycon
c, Sort
t]
  | FTycon -> Bool
isListTC FTycon
c       = Doc -> Doc
brackets forall a b. (a -> b) -> a -> b
$ Sort -> Doc
toFixSort Sort
t
toFixFApp [Sort]
ts         = Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> Doc
intersperse (String -> Doc
text String
"") (Sort -> Doc
toFixSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
ts)

instance Fixpoint FTycon where
  toFix :: FTycon -> Doc
toFix (TC LocSymbol
s TCInfo
_)       = forall a. Fixpoint a => a -> Doc
toFix (forall a. Located a -> a
val LocSymbol
s)

instance Fixpoint DataField where
  toFix :: DataField -> Doc
toFix (DField LocSymbol
x Sort
t) = forall a. Fixpoint a => a -> Doc
toFix LocSymbol
x Doc -> Doc -> Doc
<+> String -> Doc
text String
":" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Sort
t

instance Fixpoint DataCtor where
  toFix :: DataCtor -> Doc
toFix (DCtor LocSymbol
x [DataField]
flds) = forall a. Fixpoint a => a -> Doc
toFix LocSymbol
x Doc -> Doc -> Doc
<+> Doc -> Doc
braces (Doc -> [Doc] -> Doc
intersperse Doc
comma (forall a. Fixpoint a => a -> Doc
toFix forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataField]
flds))

instance Fixpoint DataDecl where
  toFix :: DataDecl -> Doc
toFix (DDecl FTycon
tc Int
n [DataCtor]
ctors) = [Doc] -> Doc
vcat ([Doc
header] forall a. [a] -> [a] -> [a]
++ [Doc]
body forall a. [a] -> [a] -> [a]
++ [Doc
footer])
    where
      header :: Doc
header               = {- text "data" <+> -} forall a. Fixpoint a => a -> Doc
toFix FTycon
tc Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Int
n Doc -> Doc -> Doc
<+> String -> Doc
text String
"= ["
      body :: [Doc]
body                 = [Int -> Doc -> Doc
nest Int
2 (String -> Doc
text String
"|" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix DataCtor
ct) | DataCtor
ct <- [DataCtor]
ctors]
      footer :: Doc
footer               = String -> Doc
text String
"]"

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

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

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

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

-------------------------------------------------------------------------
-- | Exported Basic Sorts -----------------------------------------------
-------------------------------------------------------------------------

boolSort, intSort, realSort, strSort, charSort, funcSort :: Sort
boolSort :: Sort
boolSort = FTycon -> Sort
fTyconSort FTycon
boolFTyCon
charSort :: Sort
charSort = FTycon -> Sort
fTyconSort FTycon
charFTyCon
strSort :: Sort
strSort  = FTycon -> Sort
fTyconSort FTycon
strFTyCon
intSort :: Sort
intSort  = FTycon -> Sort
fTyconSort FTycon
intFTyCon
realSort :: Sort
realSort = FTycon -> Sort
fTyconSort FTycon
realFTyCon
funcSort :: Sort
funcSort = FTycon -> Sort
fTyconSort FTycon
funcFTyCon

setSort :: Sort -> Sort
setSort :: Sort -> Sort
setSort    = Sort -> Sort -> Sort
FApp (FTycon -> Sort
FTC FTycon
setFTyCon)

-- bitVecSort :: Sort -> Sort
-- bitVecSort = FApp (FTC $ symbolFTycon' bitVecName)

-- bitVec32Sort :: Sort
-- bitVec32Sort = bitVecSort (FTC (symbolFTycon' size32Name))
--
-- bitVec64Sort :: Sort
-- bitVec64Sort = bitVecSort (FTC (symbolFTycon' size64Name))

bitVecSort :: Int -> Sort
bitVecSort :: Int -> Sort
bitVecSort Int
i = Sort -> Sort -> Sort
FApp (FTycon -> Sort
FTC forall a b. (a -> b) -> a -> b
$ Symbol -> FTycon
symbolFTycon' Symbol
bitVecName) (Int -> Sort
FVar Int
i)

sizedBitVecSort :: Symbol -> Sort
sizedBitVecSort :: Symbol -> Sort
sizedBitVecSort Symbol
i = Sort -> Sort -> Sort
FApp (FTycon -> Sort
FTC forall a b. (a -> b) -> a -> b
$ Symbol -> FTycon
symbolFTycon' Symbol
bitVecName) (FTycon -> Sort
FTC forall a b. (a -> b) -> a -> b
$ Symbol -> FTycon
symbolFTycon' Symbol
i)

mapSort :: Sort -> Sort -> Sort
mapSort :: Sort -> Sort -> Sort
mapSort = Sort -> Sort -> Sort
FApp forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Sort -> Sort
FApp (FTycon -> Sort
FTC (Symbol -> FTycon
symbolFTycon' Symbol
mapConName))

symbolFTycon' :: Symbol -> FTycon
symbolFTycon' :: Symbol -> FTycon
symbolFTycon' = LocSymbol -> FTycon
symbolFTycon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Located a
dummyLoc

fTyconSort :: FTycon -> Sort
fTyconSort :: FTycon -> Sort
fTyconSort FTycon
c
  | FTycon
c forall a. Eq a => a -> a -> Bool
== FTycon
intFTyCon  = Sort
FInt
  | FTycon
c forall a. Eq a => a -> a -> Bool
== FTycon
realFTyCon = Sort
FReal
  | FTycon
c forall a. Eq a => a -> a -> Bool
== FTycon
numFTyCon  = Sort
FNum
  | Bool
otherwise       = FTycon -> Sort
FTC FTycon
c

basicSorts :: [Sort]
basicSorts :: [Sort]
basicSorts = [Sort
FInt, Sort
boolSort]

type SortSubst = M.HashMap Symbol Sort

mkSortSubst :: [(Symbol, Sort)] -> SortSubst
mkSortSubst :: [(Symbol, Sort)] -> SortSubst
mkSortSubst = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList

------------------------------------------------------------------------
sortSubst                 :: SortSubst -> Sort -> Sort
------------------------------------------------------------------------
sortSubst :: SortSubst -> Sort -> Sort
sortSubst SortSubst
θ t :: Sort
t@(FObj Symbol
x)    = forall a. a -> Maybe a -> a
fromMaybe Sort
t (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
x SortSubst
θ)
sortSubst SortSubst
θ (FFunc Sort
t1 Sort
t2) = Sort -> Sort -> Sort
FFunc (SortSubst -> Sort -> Sort
sortSubst SortSubst
θ Sort
t1) (SortSubst -> Sort -> Sort
sortSubst SortSubst
θ Sort
t2)
sortSubst SortSubst
θ (FApp Sort
t1 Sort
t2)  = Sort -> Sort -> Sort
FApp  (SortSubst -> Sort -> Sort
sortSubst SortSubst
θ Sort
t1) (SortSubst -> Sort -> Sort
sortSubst SortSubst
θ Sort
t2)
sortSubst SortSubst
θ (FAbs Int
i Sort
t)    = Int -> Sort -> Sort
FAbs Int
i (SortSubst -> Sort -> Sort
sortSubst SortSubst
θ Sort
t)
sortSubst SortSubst
_  Sort
t            = Sort
t

-- instance (S.Store a) => S.Store (TCEmb a)
instance S.Store TCArgs
instance S.Store FTycon
instance S.Store TCInfo
instance S.Store Sort
instance S.Store DataField
instance S.Store DataCtor
instance S.Store DataDecl
instance S.Store Sub

-- | We need the Binary instances for LH's spec serialization
instance B.Binary TCInfo
instance B.Binary FTycon
instance B.Binary Sort
instance (Eq a, Hashable a, B.Binary (M.HashMap a (Sort, TCArgs))) => B.Binary (TCEmb a)

instance NFData FTycon where
  rnf :: FTycon -> ()
rnf (TC LocSymbol
x TCInfo
i) = LocSymbol
x seq :: forall a b. a -> b -> b
`seq` TCInfo
i seq :: forall a b. a -> b -> b
`seq` ()

instance (NFData a) => NFData (TCEmb a)
instance NFData TCArgs
instance NFData TCInfo
instance NFData Sort
instance NFData DataField
instance NFData DataCtor
instance NFData DataDecl
instance NFData Sub

instance Semigroup Sort where
  Sort
t1 <> :: Sort -> Sort -> Sort
<> Sort
t2
    | Sort
t1 forall a. Eq a => a -> a -> Bool
== forall a. Monoid a => a
mempty  = Sort
t2
    | Sort
t2 forall a. Eq a => a -> a -> Bool
== forall a. Monoid a => a
mempty  = Sort
t1
    | Sort
t1 forall a. Eq a => a -> a -> Bool
== Sort
t2      = Sort
t1
    | Bool
otherwise     = forall a. HasCallStack => String -> a
errorstar forall a b. (a -> b) -> a -> b
$ String
"mappend-sort: conflicting sorts t1 =" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Sort
t1 forall a. [a] -> [a] -> [a]
++ String
" t2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Sort
t2

instance Monoid Sort where
  mempty :: Sort
mempty  = Symbol -> Sort
FObj Symbol
"any"
  mappend :: Sort -> Sort -> Sort
mappend = forall a. Semigroup a => a -> a -> a
(<>)

-------------------------------------------------------------------------------
-- | Embedding stuff as Sorts
-------------------------------------------------------------------------------
newtype TCEmb a = TCE (M.HashMap a (Sort, TCArgs))
  deriving (TCEmb a -> TCEmb a -> Bool
forall a. Eq a => TCEmb a -> TCEmb a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TCEmb a -> TCEmb a -> Bool
$c/= :: forall a. Eq a => TCEmb a -> TCEmb a -> Bool
== :: TCEmb a -> TCEmb a -> Bool
$c== :: forall a. Eq a => TCEmb a -> TCEmb a -> Bool
Eq, Int -> TCEmb a -> ShowS
forall a. Show a => Int -> TCEmb a -> ShowS
forall a. Show a => [TCEmb a] -> ShowS
forall a. Show a => TCEmb a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TCEmb a] -> ShowS
$cshowList :: forall a. Show a => [TCEmb a] -> ShowS
show :: TCEmb a -> String
$cshow :: forall a. Show a => TCEmb a -> String
showsPrec :: Int -> TCEmb a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> TCEmb a -> ShowS
Show, TCEmb a -> DataType
TCEmb a -> Constr
forall {a}. (Data a, Hashable a) => Typeable (TCEmb a)
forall a. (Data a, Hashable a) => TCEmb a -> DataType
forall a. (Data a, Hashable a) => TCEmb a -> Constr
forall a.
(Data a, Hashable a) =>
(forall b. Data b => b -> b) -> TCEmb a -> TCEmb a
forall a u.
(Data a, Hashable a) =>
Int -> (forall d. Data d => d -> u) -> TCEmb a -> u
forall a u.
(Data a, Hashable a) =>
(forall d. Data d => d -> u) -> TCEmb a -> [u]
forall a r r'.
(Data a, Hashable a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TCEmb a -> r
forall a r r'.
(Data a, Hashable a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TCEmb a -> r
forall a (m :: * -> *).
(Data a, Hashable a, Monad m) =>
(forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
forall a (m :: * -> *).
(Data a, Hashable a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
forall a (c :: * -> *).
(Data a, Hashable a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TCEmb a)
forall a (c :: * -> *).
(Data a, Hashable a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TCEmb a -> c (TCEmb a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Hashable a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (TCEmb a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Hashable a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TCEmb a))
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 (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TCEmb a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TCEmb a -> c (TCEmb a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (TCEmb a))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, Hashable a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, Hashable a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Hashable a, Monad m) =>
(forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TCEmb a -> u
$cgmapQi :: forall a u.
(Data a, Hashable a) =>
Int -> (forall d. Data d => d -> u) -> TCEmb a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> TCEmb a -> [u]
$cgmapQ :: forall a u.
(Data a, Hashable a) =>
(forall d. Data d => d -> u) -> TCEmb a -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TCEmb a -> r
$cgmapQr :: forall a r r'.
(Data a, Hashable a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TCEmb a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TCEmb a -> r
$cgmapQl :: forall a r r'.
(Data a, Hashable a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TCEmb a -> r
gmapT :: (forall b. Data b => b -> b) -> TCEmb a -> TCEmb a
$cgmapT :: forall a.
(Data a, Hashable a) =>
(forall b. Data b => b -> b) -> TCEmb a -> TCEmb a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TCEmb a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Hashable a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TCEmb a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (TCEmb a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Hashable a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (TCEmb a))
dataTypeOf :: TCEmb a -> DataType
$cdataTypeOf :: forall a. (Data a, Hashable a) => TCEmb a -> DataType
toConstr :: TCEmb a -> Constr
$ctoConstr :: forall a. (Data a, Hashable a) => TCEmb a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TCEmb a)
$cgunfold :: forall a (c :: * -> *).
(Data a, Hashable a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TCEmb a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TCEmb a -> c (TCEmb a)
$cgfoldl :: forall a (c :: * -> *).
(Data a, Hashable a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TCEmb a -> c (TCEmb a)
Data, Typeable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (TCEmb a) x -> TCEmb a
forall a x. TCEmb a -> Rep (TCEmb a) x
$cto :: forall a x. Rep (TCEmb a) x -> TCEmb a
$cfrom :: forall a x. TCEmb a -> Rep (TCEmb a) x
Generic)

instance Hashable a => Hashable (TCEmb a)
instance PPrint a => PPrint (TCEmb a) where
  pprintTidy :: Tidy -> TCEmb a -> Doc
pprintTidy Tidy
k = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TCEmb a -> [(a, (Sort, TCArgs))]
tceToList


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

instance Hashable TCArgs
instance B.Binary TCArgs

tceInsertWith :: (Eq a, Hashable a) => (Sort -> Sort -> Sort) -> a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
tceInsertWith :: forall a.
(Eq a, Hashable a) =>
(Sort -> Sort -> Sort) -> a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
tceInsertWith Sort -> Sort -> Sort
f a
k Sort
t TCArgs
a (TCE HashMap a (Sort, TCArgs)
m) = forall a. HashMap a (Sort, TCArgs) -> TCEmb a
TCE (forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
M.insertWith (Sort, TCArgs) -> (Sort, TCArgs) -> (Sort, TCArgs)
ff a
k (Sort
t, TCArgs
a) HashMap a (Sort, TCArgs)
m)
  where
    ff :: (Sort, TCArgs) -> (Sort, TCArgs) -> (Sort, TCArgs)
ff (Sort
t1, TCArgs
a1) (Sort
t2, TCArgs
a2)      = (Sort -> Sort -> Sort
f Sort
t1 Sort
t2, TCArgs
a1 forall a. Semigroup a => a -> a -> a
<> TCArgs
a2)

instance Semigroup TCArgs where
  TCArgs
NoArgs <> :: TCArgs -> TCArgs -> TCArgs
<> TCArgs
NoArgs = TCArgs
NoArgs
  TCArgs
_      <> TCArgs
_      = TCArgs
WithArgs

instance Monoid TCArgs where
  mempty :: TCArgs
mempty = TCArgs
NoArgs
  mappend :: TCArgs -> TCArgs -> TCArgs
mappend = forall a. Semigroup a => a -> a -> a
(<>)

instance PPrint TCArgs where
  pprintTidy :: Tidy -> TCArgs -> Doc
pprintTidy Tidy
_ TCArgs
WithArgs = Doc
"*"
  pprintTidy Tidy
_ TCArgs
NoArgs   = Doc
""

tceInsert :: (Eq a, Hashable a) => a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
tceInsert :: forall a.
(Eq a, Hashable a) =>
a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
tceInsert a
k Sort
t TCArgs
a (TCE HashMap a (Sort, TCArgs)
m) = forall a. HashMap a (Sort, TCArgs) -> TCEmb a
TCE (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert a
k (Sort
t, TCArgs
a) HashMap a (Sort, TCArgs)
m)

tceLookup :: (Eq a, Hashable a) => a -> TCEmb a -> Maybe (Sort, TCArgs)
tceLookup :: forall a.
(Eq a, Hashable a) =>
a -> TCEmb a -> Maybe (Sort, TCArgs)
tceLookup a
k (TCE HashMap a (Sort, TCArgs)
m) = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup a
k HashMap a (Sort, TCArgs)
m

instance (Eq a, Hashable a) => Semigroup (TCEmb a) where
  (TCE HashMap a (Sort, TCArgs)
m1) <> :: TCEmb a -> TCEmb a -> TCEmb a
<> (TCE HashMap a (Sort, TCArgs)
m2) = forall a. HashMap a (Sort, TCArgs) -> TCEmb a
TCE (HashMap a (Sort, TCArgs)
m1 forall a. Semigroup a => a -> a -> a
<> HashMap a (Sort, TCArgs)
m2)

instance (Eq a, Hashable a) => Monoid (TCEmb a) where
  mempty :: TCEmb a
mempty  = forall a. HashMap a (Sort, TCArgs) -> TCEmb a
TCE forall a. Monoid a => a
mempty
  mappend :: TCEmb a -> TCEmb a -> TCEmb a
mappend = forall a. Semigroup a => a -> a -> a
(<>)


tceMap :: (Eq b, Hashable b) => (a -> b) -> TCEmb a -> TCEmb b
tceMap :: forall b a. (Eq b, Hashable b) => (a -> b) -> TCEmb a -> TCEmb b
tceMap a -> b
f = forall a. (Eq a, Hashable a) => [(a, (Sort, TCArgs))] -> TCEmb a
tceFromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst a -> b
f) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TCEmb a -> [(a, (Sort, TCArgs))]
tceToList

tceFromList :: (Eq a, Hashable a) => [(a, (Sort, TCArgs))] -> TCEmb a
tceFromList :: forall a. (Eq a, Hashable a) => [(a, (Sort, TCArgs))] -> TCEmb a
tceFromList = forall a. HashMap a (Sort, TCArgs) -> TCEmb a
TCE forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList

tceToList :: TCEmb a -> [(a, (Sort, TCArgs))]
tceToList :: forall a. TCEmb a -> [(a, (Sort, TCArgs))]
tceToList (TCE HashMap a (Sort, TCArgs)
m) = forall k v. HashMap k v -> [(k, v)]
M.toList HashMap a (Sort, TCArgs)
m

tceMember :: (Eq a, Hashable a) => a -> TCEmb a -> Bool
tceMember :: forall a. (Eq a, Hashable a) => a -> TCEmb a -> Bool
tceMember a
k (TCE HashMap a (Sort, TCArgs)
m) = forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member a
k HashMap a (Sort, TCArgs)
m