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

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

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

instance Eq FTycon where
  (TC LocSymbol
s TCInfo
_) == :: FTycon -> FTycon -> Bool
== (TC LocSymbol
s' TCInfo
_) = LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
s Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== LocSymbol -> Symbol
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
(TCInfo -> TCInfo -> Bool)
-> (TCInfo -> TCInfo -> Bool) -> Eq TCInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TCInfo -> TCInfo -> Bool
== :: TCInfo -> TCInfo -> Bool
$c/= :: TCInfo -> TCInfo -> Bool
/= :: TCInfo -> TCInfo -> Bool
Eq, Eq TCInfo
Eq TCInfo =>
(TCInfo -> TCInfo -> Ordering)
-> (TCInfo -> TCInfo -> Bool)
-> (TCInfo -> TCInfo -> Bool)
-> (TCInfo -> TCInfo -> Bool)
-> (TCInfo -> TCInfo -> Bool)
-> (TCInfo -> TCInfo -> TCInfo)
-> (TCInfo -> TCInfo -> TCInfo)
-> Ord 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
$ccompare :: TCInfo -> TCInfo -> Ordering
compare :: TCInfo -> TCInfo -> Ordering
$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
>= :: TCInfo -> TCInfo -> Bool
$cmax :: TCInfo -> TCInfo -> TCInfo
max :: TCInfo -> TCInfo -> TCInfo
$cmin :: TCInfo -> TCInfo -> TCInfo
min :: TCInfo -> TCInfo -> TCInfo
Ord, Int -> TCInfo -> ShowS
[TCInfo] -> ShowS
TCInfo -> String
(Int -> TCInfo -> ShowS)
-> (TCInfo -> String) -> ([TCInfo] -> ShowS) -> Show TCInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TCInfo -> ShowS
showsPrec :: Int -> TCInfo -> ShowS
$cshow :: TCInfo -> String
show :: TCInfo -> String
$cshowList :: [TCInfo] -> ShowS
showList :: [TCInfo] -> ShowS
Show, Typeable TCInfo
Typeable TCInfo =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TCInfo -> c TCInfo)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TCInfo)
-> (TCInfo -> Constr)
-> (TCInfo -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> TCInfo -> TCInfo)
-> (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 u. (forall d. Data d => d -> u) -> TCInfo -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TCInfo -> u)
-> (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 (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TCInfo -> m TCInfo)
-> Data TCInfo
TCInfo -> Constr
TCInfo -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TCInfo -> c TCInfo
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TCInfo -> c TCInfo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TCInfo
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TCInfo
$ctoConstr :: TCInfo -> Constr
toConstr :: TCInfo -> Constr
$cdataTypeOf :: TCInfo -> DataType
dataTypeOf :: TCInfo -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TCInfo)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TCInfo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TCInfo)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TCInfo)
$cgmapT :: (forall b. Data b => b -> b) -> TCInfo -> TCInfo
gmapT :: (forall b. Data b => b -> b) -> TCInfo -> TCInfo
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TCInfo -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TCInfo -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TCInfo -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> TCInfo -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TCInfo -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TCInfo -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TCInfo -> m TCInfo
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TCInfo -> m TCInfo
Data, Typeable, (forall x. TCInfo -> Rep TCInfo x)
-> (forall x. Rep TCInfo x -> TCInfo) -> Generic TCInfo
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
$cfrom :: forall x. TCInfo -> Rep TCInfo x
from :: forall x. TCInfo -> Rep TCInfo x
$cto :: forall x. Rep TCInfo x -> TCInfo
to :: forall x. Rep TCInfo x -> TCInfo
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 (TCInfo -> TCInfo -> TCInfo
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 = TCInfo -> TCInfo -> TCInfo
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 (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
"int"      ) TCInfo
numTcInfo
boolFTyCon :: FTycon
boolFTyCon = LocSymbol -> TCInfo -> FTycon
TC (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
"bool"     ) TCInfo
defTcInfo
realFTyCon :: FTycon
realFTyCon = LocSymbol -> TCInfo -> FTycon
TC (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
"real"     ) TCInfo
realTcInfo
numFTyCon :: FTycon
numFTyCon  = LocSymbol -> TCInfo -> FTycon
TC (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
"num"      ) TCInfo
numTcInfo
funcFTyCon :: FTycon
funcFTyCon = LocSymbol -> TCInfo -> FTycon
TC (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
"function" ) TCInfo
defTcInfo
strFTyCon :: FTycon
strFTyCon  = LocSymbol -> TCInfo -> FTycon
TC (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
forall a. IsString a => a
strConName ) TCInfo
strTcInfo
listFTyCon :: FTycon
listFTyCon = LocSymbol -> TCInfo -> FTycon
TC (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
listConName) TCInfo
defTcInfo
charFTyCon :: FTycon
charFTyCon = LocSymbol -> TCInfo -> FTycon
TC (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
forall a. IsString a => a
charConName) TCInfo
defTcInfo
setFTyCon :: FTycon
setFTyCon  = LocSymbol -> TCInfo -> FTycon
TC (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
setConName ) TCInfo
defTcInfo
mapFTyCon :: FTycon
mapFTyCon  = LocSymbol -> TCInfo -> FTycon
TC (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
mapConName ) TCInfo
defTcInfo

isListConName :: LocSymbol -> Bool
isListConName :: LocSymbol -> Bool
isListConName LocSymbol
x = Symbol
c Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
listConName Bool -> Bool -> Bool
|| Symbol
c Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
listLConName --"List"
  where
    c :: Symbol
c           = LocSymbol -> Symbol
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 = LocSymbol -> Symbol
forall a. Located a -> a
val (LocSymbol -> Symbol) -> LocSymbol -> Symbol
forall a b. (a -> b) -> a -> b
$ FTycon -> LocSymbol
fTyconSymbol FTycon
tc
  Symbol
size <- Symbol -> Symbol -> Maybe Symbol
stripPrefix Symbol
sizeName Symbol
s
  String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe (String -> Maybe Int) -> String -> Maybe Int
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 ((Symbol -> Symbol) -> LocSymbol -> LocSymbol
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Symbol -> Symbol -> Symbol
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 = isNum, tc_isReal = 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 = (Sort -> Sort -> Sort) -> Sort -> [Sort] -> Sort
forall b a. (b -> a -> b) -> b -> [a] -> b
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 (Sort -> [Sort] -> Sort)
-> (FTycon -> Sort) -> FTycon -> [Sort] -> Sort
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 Int -> Int -> Int
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 Sort -> [Sort] -> [Sort]
forall a. a -> [a] -> [a]
: [Sort]
acc) Sort
t1
    go [Sort]
acc Sort
t            = Sort
t Sort -> [Sort] -> [Sort]
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 (FTycon -> Sort) -> (LocSymbol -> FTycon) -> LocSymbol -> Sort
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    = FTycon -> Maybe FTycon
forall a. a -> Maybe a
Just FTycon
intFTyCon
sortFTycon Sort
FReal   = FTycon -> Maybe FTycon
forall a. a -> Maybe a
Just FTycon
realFTyCon
sortFTycon Sort
FNum    = FTycon -> Maybe FTycon
forall a. a -> Maybe a
Just FTycon
numFTyCon
sortFTycon (FTC FTycon
c) = FTycon -> Maybe FTycon
forall a. a -> Maybe a
Just FTycon
c
sortFTycon Sort
_       = Maybe FTycon
forall a. Maybe a
Nothing


functionSort :: Sort -> Maybe ([Int], [Sort], Sort)
functionSort :: Sort -> Maybe ([Int], [Sort], Sort)
functionSort Sort
s
  | [Int] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
is Bool -> Bool -> Bool
&& [Sort] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Sort]
ss
  = Maybe ([Int], [Sort], Sort)
forall a. Maybe a
Nothing
  | Bool
otherwise
  = ([Int], [Sort], Sort) -> Maybe ([Int], [Sort], Sort)
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
iInt -> [Int] -> [Int]
forall 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
s1Sort -> [Sort] -> [Sort]
forall a. a -> [a] -> [a]
:[Sort]
ss) Sort
s2
    go [Int]
vs [Sort]
ss Sort
t             = ([Int] -> [Int]
forall a. [a] -> [a]
reverse [Int]
vs, [Sort] -> [Sort]
forall a. [a] -> [a]
reverse [Sort]
ss, Sort
t)


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

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

sortSymbols :: Sort -> HashSet Symbol
sortSymbols :: Sort -> HashSet Symbol
sortSymbols = \case
  FObj Symbol
s -> Symbol -> HashSet Symbol
forall a. Hashable a => a -> HashSet a
HashSet.singleton Symbol
s
  FFunc Sort
t0 Sort
t1 -> HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq 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 -> HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HashSet.union (Sort -> HashSet Symbol
sortSymbols Sort
t0) (Sort -> HashSet Symbol
sortSymbols Sort
t1)
  Sort
_ -> HashSet Symbol
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
(DataField -> DataField -> Bool)
-> (DataField -> DataField -> Bool) -> Eq DataField
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DataField -> DataField -> Bool
== :: DataField -> DataField -> Bool
$c/= :: DataField -> DataField -> Bool
/= :: DataField -> DataField -> Bool
Eq, Eq DataField
Eq DataField =>
(DataField -> DataField -> Ordering)
-> (DataField -> DataField -> Bool)
-> (DataField -> DataField -> Bool)
-> (DataField -> DataField -> Bool)
-> (DataField -> DataField -> Bool)
-> (DataField -> DataField -> DataField)
-> (DataField -> DataField -> DataField)
-> Ord 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
$ccompare :: DataField -> DataField -> Ordering
compare :: DataField -> DataField -> Ordering
$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
>= :: DataField -> DataField -> Bool
$cmax :: DataField -> DataField -> DataField
max :: DataField -> DataField -> DataField
$cmin :: DataField -> DataField -> DataField
min :: DataField -> DataField -> DataField
Ord, Int -> DataField -> ShowS
[DataField] -> ShowS
DataField -> String
(Int -> DataField -> ShowS)
-> (DataField -> String)
-> ([DataField] -> ShowS)
-> Show DataField
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DataField -> ShowS
showsPrec :: Int -> DataField -> ShowS
$cshow :: DataField -> String
show :: DataField -> String
$cshowList :: [DataField] -> ShowS
showList :: [DataField] -> ShowS
Show, Typeable DataField
Typeable DataField =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> DataField -> c DataField)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DataField)
-> (DataField -> Constr)
-> (DataField -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> DataField -> DataField)
-> (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 u. (forall d. Data d => d -> u) -> DataField -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> DataField -> u)
-> (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 (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DataField -> m DataField)
-> Data DataField
DataField -> Constr
DataField -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataField -> c DataField
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataField -> c DataField
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataField
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataField
$ctoConstr :: DataField -> Constr
toConstr :: DataField -> Constr
$cdataTypeOf :: DataField -> DataType
dataTypeOf :: DataField -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataField)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataField)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataField)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataField)
$cgmapT :: (forall b. Data b => b -> b) -> DataField -> DataField
gmapT :: (forall b. Data b => b -> b) -> DataField -> DataField
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataField -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataField -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DataField -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> DataField -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataField -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataField -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
Data, Typeable, (forall x. DataField -> Rep DataField x)
-> (forall x. Rep DataField x -> DataField) -> Generic DataField
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
$cfrom :: forall x. DataField -> Rep DataField x
from :: forall x. DataField -> Rep DataField x
$cto :: forall x. Rep DataField x -> DataField
to :: forall x. Rep DataField x -> DataField
Generic)

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

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

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

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

instance Symbolic DataCtor where
  symbol :: DataCtor -> Symbol
symbol = LocSymbol -> Symbol
forall a. Located a -> a
val (LocSymbol -> Symbol)
-> (DataCtor -> LocSymbol) -> DataCtor -> Symbol
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 (DataDecl -> DataDecl) -> [DataDecl] -> [DataDecl]
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  = Sort -> Maybe Sort -> Sort
forall a. a -> Maybe a -> a
fromMaybe Sort
t (Maybe Sort -> Sort) -> Maybe Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> [(Sort, Sort)] -> Maybe Sort
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  = mapSortDataCTor f  <$> ddCtors  dd }
    mapSortDataCTor :: (Sort -> Sort) -> DataCtor -> DataCtor
mapSortDataCTor Sort -> Sort
f  DataCtor
ct = DataCtor
ct { dcFields = mapSortDataField f <$> dcFields ct }
    mapSortDataField :: (Sort -> Sort) -> DataField -> DataField
mapSortDataField Sort -> Sort
f DataField
df = DataField
df { dfSort   = f $ dfSort 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)) = LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
c Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
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 FTycon -> FTycon -> Bool
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
iInt -> Int -> Int
forall 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 (Sort -> Sort) -> Sort -> Sort
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 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ [Int] -> [Sort] -> Sort
go [Int]
is [Sort]
ss
    go [Int]
_ [Sort]
_       = String -> 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    = ([Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
as),) ([Sort] -> (Int, [Sort])) -> Maybe [Sort] -> Maybe (Int, [Sort])
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
iInt -> [Int] -> [Int]
forall 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
_)  = [Sort] -> Maybe [Sort]
forall a. a -> Maybe a
Just (Sort -> [Sort]
go Sort
z)
  where
    go :: Sort -> [Sort]
go (FFunc Sort
t1 Sort
t2) = Sort
t1 Sort -> [Sort] -> [Sort]
forall a. a -> [a] -> [a]
: Sort -> [Sort]
go Sort
t2
    go Sort
t             = [Sort
t]
bkFun Sort
_              = Maybe [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 = (Sort -> Int -> Sort) -> Sort -> [Int] -> Sort
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((Int -> Sort -> Sort) -> Sort -> Int -> Sort
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
_) = Int -> LocSymbol -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
i LocSymbol
s

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

instance Hashable Sort

newtype Sub = Sub [(Int, Sort)] deriving ((forall x. Sub -> Rep Sub x)
-> (forall x. Rep Sub x -> Sub) -> Generic Sub
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
$cfrom :: forall x. Sub -> Rep Sub x
from :: forall x. Sub -> Rep Sub x
$cto :: forall x. Rep Sub x -> Sub
to :: forall x. Rep Sub x -> Sub
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 (Int -> Doc
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)     = Symbol -> Doc
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)      = FTycon -> Doc
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 (Int -> Doc
forall a. Fixpoint a => a -> Doc
toFix Int
n Doc -> Doc -> Doc
<+> String -> Doc
text String
"," Doc -> Doc -> Doc
<+> [Sort] -> Doc
forall a. Fixpoint a => a -> Doc
toFix [Sort]
ts)
  where
    n :: Int
n                = [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
vs
    ts :: [Sort]
ts               = [Sort]
ss [Sort] -> [Sort] -> [Sort]
forall a. [a] -> [a] -> [a]
++ [Sort
s]
toFixAbsApp Sort
_ = String -> Doc
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 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Sort -> Doc
toFixSort Sort
t
toFixFApp [Sort]
ts         = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> Doc
intersperse (String -> Doc
text String
"") (Sort -> Doc
toFixSort (Sort -> Doc) -> [Sort] -> [Doc]
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
_)       = Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
s)

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

instance Fixpoint DataCtor where
  toFix :: DataCtor -> Doc
toFix (DCtor LocSymbol
x [DataField]
flds) = LocSymbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix LocSymbol
x Doc -> Doc -> Doc
<+> Doc -> Doc
braces (Doc -> [Doc] -> Doc
intersperse Doc
comma (DataField -> Doc
forall a. Fixpoint a => a -> Doc
toFix (DataField -> Doc) -> [DataField] -> [Doc]
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] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
body [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc
footer])
    where
      header :: Doc
header               = {- text "data" <+> -} FTycon -> Doc
forall a. Fixpoint a => a -> Doc
toFix FTycon
tc Doc -> Doc -> Doc
<+> Int -> 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
<+> DataCtor -> 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
_ = FTycon -> Doc
forall a. Fixpoint a => a -> Doc
toFix

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

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

instance PPrint DataDecl where
  pprintTidy :: Tidy -> DataDecl -> Doc
pprintTidy Tidy
_ = DataDecl -> Doc
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 (FTycon -> Sort) -> FTycon -> Sort
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 (FTycon -> Sort) -> FTycon -> Sort
forall a b. (a -> b) -> a -> b
$ Symbol -> FTycon
symbolFTycon' Symbol
bitVecName) (FTycon -> Sort
FTC (FTycon -> Sort) -> FTycon -> Sort
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 (Sort -> Sort -> Sort) -> (Sort -> Sort) -> Sort -> Sort -> Sort
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 (LocSymbol -> FTycon) -> (Symbol -> LocSymbol) -> Symbol -> FTycon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc

fTyconSort :: FTycon -> Sort
fTyconSort :: FTycon -> Sort
fTyconSort FTycon
c
  | FTycon
c FTycon -> FTycon -> Bool
forall a. Eq a => a -> a -> Bool
== FTycon
intFTyCon  = Sort
FInt
  | FTycon
c FTycon -> FTycon -> Bool
forall a. Eq a => a -> a -> Bool
== FTycon
realFTyCon = Sort
FReal
  | FTycon
c FTycon -> FTycon -> Bool
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 = [(Symbol, Sort)] -> SortSubst
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)    = Sort -> Maybe Sort -> Sort
forall a. a -> Maybe a -> a
fromMaybe Sort
t (Symbol -> SortSubst -> Maybe Sort
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 LocSymbol -> () -> ()
forall a b. a -> b -> b
`seq` TCInfo
i TCInfo -> () -> ()
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 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
forall a. Monoid a => a
mempty  = Sort
t2
    | Sort
t2 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
forall a. Monoid a => a
mempty  = Sort
t1
    | Sort
t1 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t2      = Sort
t1
    | Bool
otherwise     = String -> Sort
forall a. HasCallStack => String -> a
errorstar (String -> Sort) -> String -> Sort
forall a b. (a -> b) -> a -> b
$ String
"mappend-sort: conflicting sorts t1 =" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sort -> String
forall a. Show a => a -> String
show Sort
t1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" t2 = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sort -> String
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 = Sort -> Sort -> Sort
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
(TCEmb a -> TCEmb a -> Bool)
-> (TCEmb a -> TCEmb a -> Bool) -> Eq (TCEmb a)
forall a. Eq a => TCEmb a -> TCEmb a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: TCEmb a -> TCEmb a -> Bool
Eq, Int -> TCEmb a -> ShowS
[TCEmb a] -> ShowS
TCEmb a -> String
(Int -> TCEmb a -> ShowS)
-> (TCEmb a -> String) -> ([TCEmb a] -> ShowS) -> Show (TCEmb a)
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
$cshowsPrec :: forall a. Show a => Int -> TCEmb a -> ShowS
showsPrec :: Int -> TCEmb a -> ShowS
$cshow :: forall a. Show a => TCEmb a -> String
show :: TCEmb a -> String
$cshowList :: forall a. Show a => [TCEmb a] -> ShowS
showList :: [TCEmb a] -> ShowS
Show, Typeable (TCEmb a)
Typeable (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 (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (TCEmb a))
-> (TCEmb a -> Constr)
-> (TCEmb a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (TCEmb a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TCEmb a)))
-> ((forall b. Data b => b -> b) -> TCEmb a -> TCEmb a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TCEmb a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TCEmb a -> r)
-> (forall u. (forall d. Data d => d -> u) -> TCEmb a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TCEmb a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a))
-> Data (TCEmb a)
TCEmb a -> Constr
TCEmb a -> DataType
(forall b. Data b => b -> b) -> TCEmb a -> TCEmb a
forall a. (Data a, Hashable a) => Typeable (TCEmb a)
forall a. (Data a, Hashable a) => TCEmb a -> Constr
forall a. (Data a, Hashable a) => TCEmb a -> DataType
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 u. Int -> (forall d. Data d => d -> u) -> TCEmb a -> u
forall u. (forall d. Data d => d -> u) -> TCEmb a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TCEmb a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TCEmb a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb 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))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TCEmb a -> 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)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TCEmb a)
$ctoConstr :: forall a. (Data a, Hashable a) => TCEmb a -> Constr
toConstr :: TCEmb a -> Constr
$cdataTypeOf :: forall a. (Data a, Hashable a) => TCEmb a -> DataType
dataTypeOf :: TCEmb a -> DataType
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Hashable a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (TCEmb a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> 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))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TCEmb a))
$cgmapT :: forall a.
(Data a, Hashable a) =>
(forall b. Data b => b -> b) -> TCEmb a -> TCEmb a
gmapT :: (forall b. Data b => b -> b) -> TCEmb a -> TCEmb a
$cgmapQl :: 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
$cgmapQr :: forall a r r'.
(Data a, Hashable a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TCEmb a -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TCEmb a -> r
$cgmapQ :: forall a u.
(Data a, Hashable a) =>
(forall d. Data d => d -> u) -> TCEmb a -> [u]
gmapQ :: forall u. (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
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TCEmb a -> u
$cgmapM :: forall a (m :: * -> *).
(Data a, Hashable a, Monad 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)
$cgmapMp :: 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)
$cgmapMo :: forall a (m :: * -> *).
(Data a, Hashable a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
Data, Typeable, (forall x. TCEmb a -> Rep (TCEmb a) x)
-> (forall x. Rep (TCEmb a) x -> TCEmb a) -> Generic (TCEmb a)
forall x. Rep (TCEmb a) x -> TCEmb a
forall x. TCEmb a -> Rep (TCEmb a) x
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
$cfrom :: forall a x. TCEmb a -> Rep (TCEmb a) x
from :: forall x. TCEmb a -> Rep (TCEmb a) x
$cto :: forall a x. Rep (TCEmb a) x -> TCEmb a
to :: forall x. Rep (TCEmb a) x -> TCEmb a
Generic)

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


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