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

-- | This module contains the data types, operations and
--   serialization functions for representing Fixpoint's
--   implication (i.e. subtyping) and well-formedness
--   constraints in Haskell. The actual constraint
--   solving is done by the `fixpoint.native` which
--   is written in Ocaml.

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
  , setSort, bitVecSort, mapSort, charSort

  , listFTyCon
  , isListTC
  , sizeBv
  , isFirstOrder
  , mappendFTC
  , fTyconSymbol, symbolFTycon, fTyconSort, symbolNumInfoFTyCon
  , fTyconSelfSort
  , fApp
  , fAppTC
  , fObj
  , unFApp
  , unAbs
  , sortAbs

  , mkSortSubst
  , sortSubst
  , functionSort
  , mkFFunc
  , bkFFunc
  , mkPoly

  , 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.Binary as B
import           Data.Generics             (Data)
import           Data.Typeable             (Typeable)
import           GHC.Generics              (Generic)

#if !MIN_VERSION_base(4,14,0)
import           Data.Semigroup            (Semigroup (..))
#endif

import           Data.Hashable
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

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

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

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

mappendFTC :: FTycon -> FTycon -> FTycon
mappendFTC :: FTycon -> FTycon -> FTycon
mappendFTC (TC LocSymbol
x TCInfo
i1) (TC LocSymbol
_ TCInfo
i2) = LocSymbol -> TCInfo -> FTycon
TC LocSymbol
x (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
  | Symbol
s Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
size32Name = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
32
  | Symbol
s Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
size64Name = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
64
  | Bool
otherwise       = Maybe Int
forall a. Maybe a
Nothing
  where
    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

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 (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 :: Bool
tc_isNum = Bool
isNum, tc_isReal :: Bool
tc_isReal = Bool
isReal}



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

fApp :: Sort -> [Sort] -> Sort
fApp :: Sort -> [Sort] -> Sort
fApp = (Sort -> Sort -> Sort) -> Sort -> [Sort] -> Sort
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 (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
is Bool -> Bool -> Bool
&& [Sort] -> 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
/= :: Sort -> Sort -> Bool
$c/= :: Sort -> Sort -> Bool
== :: Sort -> Sort -> Bool
$c== :: 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
min :: Sort -> Sort -> Sort
$cmin :: Sort -> Sort -> Sort
max :: Sort -> Sort -> Sort
$cmax :: Sort -> Sort -> Sort
>= :: Sort -> Sort -> Bool
$c>= :: Sort -> Sort -> Bool
> :: Sort -> Sort -> Bool
$c> :: Sort -> Sort -> Bool
<= :: Sort -> Sort -> Bool
$c<= :: Sort -> Sort -> Bool
< :: Sort -> Sort -> Bool
$c< :: Sort -> Sort -> Bool
compare :: Sort -> Sort -> Ordering
$ccompare :: Sort -> Sort -> Ordering
$cp1Ord :: Eq 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
showList :: [Sort] -> ShowS
$cshowList :: [Sort] -> ShowS
show :: Sort -> String
$cshow :: Sort -> String
showsPrec :: Int -> Sort -> ShowS
$cshowsPrec :: Int -> Sort -> ShowS
Show, Typeable Sort
DataType
Constr
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 -> DataType
Sort -> Constr
(forall b. Data b => b -> b) -> Sort -> Sort
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sort -> c Sort
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cFApp :: Constr
$cFTC :: Constr
$cFAbs :: Constr
$cFFunc :: Constr
$cFVar :: Constr
$cFObj :: Constr
$cFFrac :: Constr
$cFNum :: Constr
$cFReal :: Constr
$cFInt :: Constr
$tSort :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Sort -> m Sort
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
gmapMp :: (forall d. Data d => d -> m d) -> Sort -> m Sort
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
gmapM :: (forall d. Data d => d -> m d) -> Sort -> m Sort
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
gmapQi :: Int -> (forall d. Data d => d -> u) -> Sort -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sort -> u
gmapQ :: (forall d. Data d => d -> u) -> Sort -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Sort -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r
gmapT :: (forall b. Data b => b -> b) -> Sort -> Sort
$cgmapT :: (forall b. Data b => b -> b) -> Sort -> Sort
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sort)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sort)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Sort)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sort)
dataTypeOf :: Sort -> DataType
$cdataTypeOf :: Sort -> DataType
toConstr :: Sort -> Constr
$ctoConstr :: Sort -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sort
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sort
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sort -> c Sort
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sort -> c Sort
$cp1Data :: Typeable 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
$cto :: forall x. Rep Sort x -> Sort
$cfrom :: forall x. Sort -> Rep Sort x
Generic)

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

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

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


instance Loc DataDecl where
    srcSpan :: DataDecl -> SrcSpan
srcSpan (DDecl FTycon
ty Int
_ [DataCtor]
_) = 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 :: [DataCtor]
ddCtors  = (Sort -> Sort) -> DataCtor -> DataCtor
mapSortDataCTor Sort -> Sort
f  (DataCtor -> DataCtor) -> [DataCtor] -> [DataCtor]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataDecl -> [DataCtor]
ddCtors  DataDecl
dd }
    mapSortDataCTor :: (Sort -> Sort) -> DataCtor -> DataCtor
mapSortDataCTor Sort -> Sort
f  DataCtor
ct = DataCtor
ct { dcFields :: [DataField]
dcFields = (Sort -> Sort) -> DataField -> DataField
mapSortDataField Sort -> Sort
f (DataField -> DataField) -> [DataField] -> [DataField]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCtor -> [DataField]
dcFields DataCtor
ct }
    mapSortDataField :: (Sort -> Sort) -> DataField -> DataField
mapSortDataField Sort -> Sort
f DataField
df = DataField
df { dfSort :: Sort
dfSort   = Sort -> Sort
f (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ DataField -> Sort
dfSort DataField
df }

isFirstOrder, isFunction :: Sort -> Bool
isFirstOrder :: Sort -> Bool
isFirstOrder (FFunc Sort
sx Sort
s) = Bool -> Bool
not (Sort -> Bool
isFunction Sort
sx) Bool -> Bool -> Bool
&& Sort -> Bool
isFirstOrder Sort
s
isFirstOrder (FAbs Int
_ Sort
s)   = Sort -> Bool
isFirstOrder Sort
s
isFirstOrder (FApp Sort
s1 Sort
s2) = (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Sort -> Bool
isFunction Sort
s1) Bool -> Bool -> Bool
&& (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ 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 (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 (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
$cto :: forall x. Rep Sub x -> Sub
$cfrom :: forall x. Sub -> Rep Sub x
Generic)

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

toFixSort :: Sort -> Doc
toFixSort :: Sort -> Doc
toFixSort (FVar Int
i)     = String -> Doc
text String
"@" Doc -> Doc -> Doc
<-> Doc -> Doc
parens (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
t = 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
    Just ([Int]
vs, [Sort]
ss, Sort
s) = Sort -> Maybe ([Int], [Sort], Sort)
functionSort Sort
t
    n :: Int
n                = [Int] -> 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]

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
bitVecSort :: Sort
bitVecSort = 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
size32Name)

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 (B.Binary a) => B.Binary (TCEmb a) 
instance B.Binary TCArgs 
instance B.Binary FTycon
instance B.Binary TCInfo
instance B.Binary Sort
instance B.Binary DataField
instance B.Binary DataCtor
instance B.Binary DataDecl
instance B.Binary Sub

instance NFData FTycon where
  rnf :: FTycon -> ()
rnf (TC LocSymbol
x TCInfo
i) = LocSymbol
x LocSymbol -> () -> ()
`seq` TCInfo
i TCInfo -> () -> ()
`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
/= :: TCEmb a -> TCEmb a -> Bool
$c/= :: forall a. Eq a => TCEmb a -> TCEmb a -> Bool
== :: TCEmb a -> TCEmb a -> Bool
$c== :: forall a. Eq a => TCEmb a -> TCEmb a -> Bool
Eq, Int -> TCEmb a -> ShowS
[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
showList :: [TCEmb a] -> ShowS
$cshowList :: forall a. Show a => [TCEmb a] -> ShowS
show :: TCEmb a -> String
$cshow :: forall a. Show a => TCEmb a -> String
showsPrec :: Int -> TCEmb a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> TCEmb a -> ShowS
Show, Typeable (TCEmb a)
DataType
Constr
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 -> DataType
TCEmb a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (TCEmb a))
(forall b. Data b => b -> b) -> TCEmb a -> TCEmb a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TCEmb a -> c (TCEmb a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TCEmb a)
forall a. (Data a, Eq a, Hashable a) => Typeable (TCEmb a)
forall a. (Data a, Eq a, Hashable a) => TCEmb a -> DataType
forall a. (Data a, Eq a, Hashable a) => TCEmb a -> Constr
forall a.
(Data a, Eq a, Hashable a) =>
(forall b. Data b => b -> b) -> TCEmb a -> TCEmb a
forall a u.
(Data a, Eq a, Hashable a) =>
Int -> (forall d. Data d => d -> u) -> TCEmb a -> u
forall a u.
(Data a, Eq a, Hashable a) =>
(forall d. Data d => d -> u) -> TCEmb a -> [u]
forall a r r'.
(Data a, Eq a, Hashable a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TCEmb a -> r
forall a r r'.
(Data a, Eq a, Hashable a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TCEmb a -> r
forall a (m :: * -> *).
(Data a, Eq a, Hashable a, Monad m) =>
(forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
forall a (m :: * -> *).
(Data a, Eq a, Hashable a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
forall a (c :: * -> *).
(Data a, Eq 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, Eq 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, Eq a, Hashable a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (TCEmb a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Eq 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))
$cTCE :: Constr
$tTCEmb :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, Eq a, Hashable a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
gmapMp :: (forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, Eq a, Hashable a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
gmapM :: (forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Eq a, Hashable a, Monad m) =>
(forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> TCEmb a -> u
$cgmapQi :: forall a u.
(Data a, Eq a, Hashable a) =>
Int -> (forall d. Data d => d -> u) -> TCEmb a -> u
gmapQ :: (forall d. Data d => d -> u) -> TCEmb a -> [u]
$cgmapQ :: forall a u.
(Data a, Eq a, Hashable a) =>
(forall d. Data d => d -> u) -> TCEmb a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TCEmb a -> r
$cgmapQr :: forall a r r'.
(Data a, Eq a, Hashable a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TCEmb a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TCEmb a -> r
$cgmapQl :: forall a r r'.
(Data a, Eq a, Hashable a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TCEmb a -> r
gmapT :: (forall b. Data b => b -> b) -> TCEmb a -> TCEmb a
$cgmapT :: forall a.
(Data a, Eq a, Hashable a) =>
(forall b. Data b => b -> b) -> TCEmb a -> TCEmb a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TCEmb a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Eq a, Hashable a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TCEmb a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (TCEmb a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Eq a, Hashable a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (TCEmb a))
dataTypeOf :: TCEmb a -> DataType
$cdataTypeOf :: forall a. (Data a, Eq a, Hashable a) => TCEmb a -> DataType
toConstr :: TCEmb a -> Constr
$ctoConstr :: forall a. (Data a, Eq a, Hashable a) => TCEmb a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TCEmb a)
$cgunfold :: forall a (c :: * -> *).
(Data a, Eq a, Hashable a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TCEmb a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TCEmb a -> c (TCEmb a)
$cgfoldl :: forall a (c :: * -> *).
(Data a, Eq a, Hashable a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TCEmb a -> c (TCEmb a)
$cp1Data :: forall a. (Data a, Eq a, Hashable a) => Typeable (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
$cto :: forall a x. Rep (TCEmb a) x -> TCEmb a
$cfrom :: forall a x. TCEmb a -> Rep (TCEmb a) x
Generic) 

instance Hashable a => Hashable (TCEmb a)

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

instance Hashable TCArgs 

tceInsertWith :: (Eq a, Hashable a) => (Sort -> Sort -> Sort) -> a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
tceInsertWith :: (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 :: 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 :: 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 :: (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 (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 :: [(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 :: 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 :: 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