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

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

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

module Language.Fixpoint.Types.Sorts (

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

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

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

  , isBool, isNumeric, isReal, isString, isSet, isMap, isBag, isArray, isPolyInst

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

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

  -- * Sort coercion for SMT theory encoding
  , coerceMapToArray
  , coerceSetBagToArray
  , coerceDataDecl
  ) where

import qualified Data.Store as S
import           Data.Generics             (Data)
import           Data.Typeable             (Typeable)
import           GHC.Generics              (Generic)
import           Data.Aeson
import           Data.Bifunctor (first)

import           Data.Hashable
import           Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
#if !MIN_VERSION_base(4,20,0)
import           Data.List                 (foldl')
#endif
import           Control.DeepSeq
import           Data.Maybe                (fromMaybe)
import           Language.Fixpoint.Types.Config (ElabFlags, elabSetBag)
import           Language.Fixpoint.Types.Names
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Spans
import           Language.Fixpoint.Misc
import           Text.PrettyPrint.HughesPJ.Compat
import qualified Data.HashMap.Strict       as M
import qualified Data.List                 as L
import qualified Data.Binary as B
import Text.Read (readMaybe)

data FTycon   = TC LocSymbol TCInfo deriving (Eq FTycon
Eq FTycon =>
(FTycon -> FTycon -> Ordering)
-> (FTycon -> FTycon -> Bool)
-> (FTycon -> FTycon -> Bool)
-> (FTycon -> FTycon -> Bool)
-> (FTycon -> FTycon -> Bool)
-> (FTycon -> FTycon -> FTycon)
-> (FTycon -> FTycon -> FTycon)
-> Ord FTycon
FTycon -> FTycon -> Bool
FTycon -> FTycon -> Ordering
FTycon -> FTycon -> FTycon
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FTycon -> FTycon -> Ordering
compare :: FTycon -> FTycon -> Ordering
$c< :: FTycon -> FTycon -> Bool
< :: FTycon -> FTycon -> Bool
$c<= :: FTycon -> FTycon -> Bool
<= :: FTycon -> FTycon -> Bool
$c> :: FTycon -> FTycon -> Bool
> :: FTycon -> FTycon -> Bool
$c>= :: FTycon -> FTycon -> Bool
>= :: FTycon -> FTycon -> Bool
$cmax :: FTycon -> FTycon -> FTycon
max :: FTycon -> FTycon -> FTycon
$cmin :: FTycon -> FTycon -> FTycon
min :: FTycon -> FTycon -> FTycon
Ord, Int -> FTycon -> ShowS
[FTycon] -> ShowS
FTycon -> String
(Int -> FTycon -> ShowS)
-> (FTycon -> String) -> ([FTycon] -> ShowS) -> Show FTycon
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FTycon -> ShowS
showsPrec :: Int -> FTycon -> ShowS
$cshow :: FTycon -> String
show :: FTycon -> String
$cshowList :: [FTycon] -> ShowS
showList :: [FTycon] -> ShowS
Show, Typeable FTycon
Typeable FTycon =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> FTycon -> c FTycon)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c FTycon)
-> (FTycon -> Constr)
-> (FTycon -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c FTycon))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FTycon))
-> ((forall b. Data b => b -> b) -> FTycon -> FTycon)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> FTycon -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> FTycon -> r)
-> (forall u. (forall d. Data d => d -> u) -> FTycon -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> FTycon -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> FTycon -> m FTycon)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FTycon -> m FTycon)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FTycon -> m FTycon)
-> Data FTycon
FTycon -> Constr
FTycon -> DataType
(forall b. Data b => b -> b) -> FTycon -> FTycon
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> FTycon -> u
forall u. (forall d. Data d => d -> u) -> FTycon -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FTycon -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FTycon -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FTycon -> m FTycon
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FTycon -> m FTycon
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FTycon
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FTycon -> c FTycon
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FTycon)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FTycon)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FTycon -> c FTycon
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FTycon -> c FTycon
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FTycon
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FTycon
$ctoConstr :: FTycon -> Constr
toConstr :: FTycon -> Constr
$cdataTypeOf :: FTycon -> DataType
dataTypeOf :: FTycon -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FTycon)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FTycon)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FTycon)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FTycon)
$cgmapT :: (forall b. Data b => b -> b) -> FTycon -> FTycon
gmapT :: (forall b. Data b => b -> b) -> FTycon -> FTycon
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FTycon -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FTycon -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FTycon -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FTycon -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> FTycon -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> FTycon -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FTycon -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FTycon -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FTycon -> m FTycon
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FTycon -> m FTycon
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FTycon -> m FTycon
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FTycon -> m FTycon
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FTycon -> m FTycon
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FTycon -> m FTycon
Data, Typeable, (forall x. FTycon -> Rep FTycon x)
-> (forall x. Rep FTycon x -> FTycon) -> Generic FTycon
forall x. Rep FTycon x -> FTycon
forall x. FTycon -> Rep FTycon x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FTycon -> Rep FTycon x
from :: forall x. FTycon -> Rep FTycon x
$cto :: forall x. Rep FTycon x -> FTycon
to :: forall x. Rep FTycon x -> FTycon
Generic, [FTycon] -> Value
[FTycon] -> Encoding
FTycon -> Bool
FTycon -> Value
FTycon -> Encoding
(FTycon -> Value)
-> (FTycon -> Encoding)
-> ([FTycon] -> Value)
-> ([FTycon] -> Encoding)
-> (FTycon -> Bool)
-> ToJSON FTycon
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: FTycon -> Value
toJSON :: FTycon -> Value
$ctoEncoding :: FTycon -> Encoding
toEncoding :: FTycon -> Encoding
$ctoJSONList :: [FTycon] -> Value
toJSONList :: [FTycon] -> Value
$ctoEncodingList :: [FTycon] -> Encoding
toEncodingList :: [FTycon] -> Encoding
$comitField :: FTycon -> Bool
omitField :: FTycon -> Bool
ToJSON, Maybe FTycon
Value -> Parser [FTycon]
Value -> Parser FTycon
(Value -> Parser FTycon)
-> (Value -> Parser [FTycon]) -> Maybe FTycon -> FromJSON FTycon
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: Value -> Parser FTycon
parseJSON :: Value -> Parser FTycon
$cparseJSONList :: Value -> Parser [FTycon]
parseJSONList :: Value -> Parser [FTycon]
$comittedField :: Maybe FTycon
omittedField :: Maybe FTycon
FromJSON)

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

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

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

data TCInfo = TCInfo { TCInfo -> Bool
tc_isNum :: Bool, TCInfo -> Bool
tc_isReal :: Bool, TCInfo -> Bool
tc_isString :: Bool }
  deriving (TCInfo -> TCInfo -> Bool
(TCInfo -> TCInfo -> Bool)
-> (TCInfo -> TCInfo -> Bool) -> Eq TCInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TCInfo -> TCInfo -> Bool
== :: TCInfo -> TCInfo -> Bool
$c/= :: TCInfo -> TCInfo -> Bool
/= :: TCInfo -> TCInfo -> Bool
Eq, Eq TCInfo
Eq TCInfo =>
(TCInfo -> TCInfo -> Ordering)
-> (TCInfo -> TCInfo -> Bool)
-> (TCInfo -> TCInfo -> Bool)
-> (TCInfo -> TCInfo -> Bool)
-> (TCInfo -> TCInfo -> Bool)
-> (TCInfo -> TCInfo -> TCInfo)
-> (TCInfo -> TCInfo -> TCInfo)
-> Ord TCInfo
TCInfo -> TCInfo -> Bool
TCInfo -> TCInfo -> Ordering
TCInfo -> TCInfo -> TCInfo
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: TCInfo -> TCInfo -> Ordering
compare :: TCInfo -> TCInfo -> Ordering
$c< :: TCInfo -> TCInfo -> Bool
< :: TCInfo -> TCInfo -> Bool
$c<= :: TCInfo -> TCInfo -> Bool
<= :: TCInfo -> TCInfo -> Bool
$c> :: TCInfo -> TCInfo -> Bool
> :: TCInfo -> TCInfo -> Bool
$c>= :: TCInfo -> TCInfo -> Bool
>= :: TCInfo -> TCInfo -> Bool
$cmax :: TCInfo -> TCInfo -> TCInfo
max :: TCInfo -> TCInfo -> TCInfo
$cmin :: TCInfo -> TCInfo -> TCInfo
min :: TCInfo -> TCInfo -> TCInfo
Ord, Int -> TCInfo -> ShowS
[TCInfo] -> ShowS
TCInfo -> String
(Int -> TCInfo -> ShowS)
-> (TCInfo -> String) -> ([TCInfo] -> ShowS) -> Show TCInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TCInfo -> ShowS
showsPrec :: Int -> TCInfo -> ShowS
$cshow :: TCInfo -> String
show :: TCInfo -> String
$cshowList :: [TCInfo] -> ShowS
showList :: [TCInfo] -> ShowS
Show, Typeable TCInfo
Typeable TCInfo =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TCInfo -> c TCInfo)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TCInfo)
-> (TCInfo -> Constr)
-> (TCInfo -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TCInfo))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TCInfo))
-> ((forall b. Data b => b -> b) -> TCInfo -> TCInfo)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TCInfo -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TCInfo -> r)
-> (forall u. (forall d. Data d => d -> u) -> TCInfo -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TCInfo -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TCInfo -> m TCInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TCInfo -> m TCInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TCInfo -> m TCInfo)
-> Data TCInfo
TCInfo -> Constr
TCInfo -> DataType
(forall b. Data b => b -> b) -> TCInfo -> TCInfo
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> TCInfo -> u
forall u. (forall d. Data d => d -> u) -> TCInfo -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TCInfo -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TCInfo -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TCInfo -> m TCInfo
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TCInfo -> m TCInfo
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TCInfo
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TCInfo -> c TCInfo
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TCInfo)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TCInfo)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TCInfo -> c TCInfo
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TCInfo -> c TCInfo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TCInfo
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TCInfo
$ctoConstr :: TCInfo -> Constr
toConstr :: TCInfo -> Constr
$cdataTypeOf :: TCInfo -> DataType
dataTypeOf :: TCInfo -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TCInfo)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TCInfo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TCInfo)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TCInfo)
$cgmapT :: (forall b. Data b => b -> b) -> TCInfo -> TCInfo
gmapT :: (forall b. Data b => b -> b) -> TCInfo -> TCInfo
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TCInfo -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TCInfo -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TCInfo -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TCInfo -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TCInfo -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> TCInfo -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TCInfo -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TCInfo -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TCInfo -> m TCInfo
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TCInfo -> m TCInfo
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TCInfo -> m TCInfo
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TCInfo -> m TCInfo
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TCInfo -> m TCInfo
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TCInfo -> m TCInfo
Data, Typeable, (forall x. TCInfo -> Rep TCInfo x)
-> (forall x. Rep TCInfo x -> TCInfo) -> Generic TCInfo
forall x. Rep TCInfo x -> TCInfo
forall x. TCInfo -> Rep TCInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TCInfo -> Rep TCInfo x
from :: forall x. TCInfo -> Rep TCInfo x
$cto :: forall x. Rep TCInfo x -> TCInfo
to :: forall x. Rep TCInfo x -> TCInfo
Generic, [TCInfo] -> Value
[TCInfo] -> Encoding
TCInfo -> Bool
TCInfo -> Value
TCInfo -> Encoding
(TCInfo -> Value)
-> (TCInfo -> Encoding)
-> ([TCInfo] -> Value)
-> ([TCInfo] -> Encoding)
-> (TCInfo -> Bool)
-> ToJSON TCInfo
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: TCInfo -> Value
toJSON :: TCInfo -> Value
$ctoEncoding :: TCInfo -> Encoding
toEncoding :: TCInfo -> Encoding
$ctoJSONList :: [TCInfo] -> Value
toJSONList :: [TCInfo] -> Value
$ctoEncodingList :: [TCInfo] -> Encoding
toEncodingList :: [TCInfo] -> Encoding
$comitField :: TCInfo -> Bool
omitField :: TCInfo -> Bool
ToJSON, Maybe TCInfo
Value -> Parser [TCInfo]
Value -> Parser TCInfo
(Value -> Parser TCInfo)
-> (Value -> Parser [TCInfo]) -> Maybe TCInfo -> FromJSON TCInfo
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: Value -> Parser TCInfo
parseJSON :: Value -> Parser TCInfo
$cparseJSONList :: Value -> Parser [TCInfo]
parseJSONList :: Value -> Parser [TCInfo]
$comittedField :: Maybe TCInfo
omittedField :: Maybe TCInfo
FromJSON)

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, bagFTyCon, 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
boolLConName) 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
bagFTyCon :: FTycon
bagFTyCon  = LocSymbol -> TCInfo -> FTycon
TC (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
bagConName  ) 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

isSetConName :: LocSymbol -> Bool
isSetConName :: LocSymbol -> Bool
isSetConName LocSymbol
x = Symbol
c Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
setConName
  where
    c :: Symbol
c           = LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x

isSetTC :: FTycon -> Bool
isSetTC :: FTycon -> Bool
isSetTC (TC LocSymbol
z TCInfo
_) = LocSymbol -> Bool
isSetConName LocSymbol
z

isMapConName :: LocSymbol -> Bool
isMapConName :: LocSymbol -> Bool
isMapConName LocSymbol
x = Symbol
c Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
mapConName
  where
    c :: Symbol
c           = LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x

isMapTC :: FTycon -> Bool
isMapTC :: FTycon -> Bool
isMapTC (TC LocSymbol
z TCInfo
_) = LocSymbol -> Bool
isMapConName LocSymbol
z

isBagConName :: LocSymbol -> Bool
isBagConName :: LocSymbol -> Bool
isBagConName LocSymbol
x = Symbol
c Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
bagConName
  where
    c :: Symbol
c           = LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x

isBagTC :: FTycon -> Bool
isBagTC :: FTycon -> Bool
isBagTC (TC LocSymbol
z TCInfo
_) = LocSymbol -> Bool
isBagConName LocSymbol
z

isArrayConName :: LocSymbol -> Bool
isArrayConName :: LocSymbol -> Bool
isArrayConName LocSymbol
x = Symbol
c Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
arrayConName
  where
    c :: Symbol
c           = LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x

isArrayTC :: FTycon -> Bool
isArrayTC :: FTycon -> Bool
isArrayTC (TC LocSymbol
z TCInfo
_) = LocSymbol -> Bool
isArrayConName LocSymbol
z

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

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

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



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

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

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

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

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

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

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

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

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


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


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

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

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

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

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

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

data DataField = DField
  { DataField -> LocSymbol
dfName :: !LocSymbol          -- ^ Field Name
  , DataField -> Sort
dfSort :: !Sort               -- ^ Field Sort
  } deriving (DataField -> DataField -> Bool
(DataField -> DataField -> Bool)
-> (DataField -> DataField -> Bool) -> Eq DataField
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DataField -> DataField -> Bool
== :: DataField -> DataField -> Bool
$c/= :: DataField -> DataField -> Bool
/= :: DataField -> DataField -> Bool
Eq, Eq DataField
Eq DataField =>
(DataField -> DataField -> Ordering)
-> (DataField -> DataField -> Bool)
-> (DataField -> DataField -> Bool)
-> (DataField -> DataField -> Bool)
-> (DataField -> DataField -> Bool)
-> (DataField -> DataField -> DataField)
-> (DataField -> DataField -> DataField)
-> Ord DataField
DataField -> DataField -> Bool
DataField -> DataField -> Ordering
DataField -> DataField -> DataField
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: DataField -> DataField -> Ordering
compare :: DataField -> DataField -> Ordering
$c< :: DataField -> DataField -> Bool
< :: DataField -> DataField -> Bool
$c<= :: DataField -> DataField -> Bool
<= :: DataField -> DataField -> Bool
$c> :: DataField -> DataField -> Bool
> :: DataField -> DataField -> Bool
$c>= :: DataField -> DataField -> Bool
>= :: DataField -> DataField -> Bool
$cmax :: DataField -> DataField -> DataField
max :: DataField -> DataField -> DataField
$cmin :: DataField -> DataField -> DataField
min :: DataField -> DataField -> DataField
Ord, Int -> DataField -> ShowS
[DataField] -> ShowS
DataField -> String
(Int -> DataField -> ShowS)
-> (DataField -> String)
-> ([DataField] -> ShowS)
-> Show DataField
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DataField -> ShowS
showsPrec :: Int -> DataField -> ShowS
$cshow :: DataField -> String
show :: DataField -> String
$cshowList :: [DataField] -> ShowS
showList :: [DataField] -> ShowS
Show, Typeable DataField
Typeable DataField =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> DataField -> c DataField)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DataField)
-> (DataField -> Constr)
-> (DataField -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DataField))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataField))
-> ((forall b. Data b => b -> b) -> DataField -> DataField)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DataField -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DataField -> r)
-> (forall u. (forall d. Data d => d -> u) -> DataField -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> DataField -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> DataField -> m DataField)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DataField -> m DataField)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DataField -> m DataField)
-> Data DataField
DataField -> Constr
DataField -> DataType
(forall b. Data b => b -> b) -> DataField -> DataField
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> DataField -> u
forall u. (forall d. Data d => d -> u) -> DataField -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataField -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataField -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataField
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataField -> c DataField
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataField)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataField)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataField -> c DataField
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataField -> c DataField
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataField
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataField
$ctoConstr :: DataField -> Constr
toConstr :: DataField -> Constr
$cdataTypeOf :: DataField -> DataType
dataTypeOf :: DataField -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataField)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataField)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataField)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataField)
$cgmapT :: (forall b. Data b => b -> b) -> DataField -> DataField
gmapT :: (forall b. Data b => b -> b) -> DataField -> DataField
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataField -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataField -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataField -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataField -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DataField -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> DataField -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataField -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataField -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataField -> m DataField
Data, Typeable, (forall x. DataField -> Rep DataField x)
-> (forall x. Rep DataField x -> DataField) -> Generic DataField
forall x. Rep DataField x -> DataField
forall x. DataField -> Rep DataField x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DataField -> Rep DataField x
from :: forall x. DataField -> Rep DataField x
$cto :: forall x. Rep DataField x -> DataField
to :: forall x. Rep DataField x -> DataField
Generic, [DataField] -> Value
[DataField] -> Encoding
DataField -> Bool
DataField -> Value
DataField -> Encoding
(DataField -> Value)
-> (DataField -> Encoding)
-> ([DataField] -> Value)
-> ([DataField] -> Encoding)
-> (DataField -> Bool)
-> ToJSON DataField
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: DataField -> Value
toJSON :: DataField -> Value
$ctoEncoding :: DataField -> Encoding
toEncoding :: DataField -> Encoding
$ctoJSONList :: [DataField] -> Value
toJSONList :: [DataField] -> Value
$ctoEncodingList :: [DataField] -> Encoding
toEncodingList :: [DataField] -> Encoding
$comitField :: DataField -> Bool
omitField :: DataField -> Bool
ToJSON, Maybe DataField
Value -> Parser [DataField]
Value -> Parser DataField
(Value -> Parser DataField)
-> (Value -> Parser [DataField])
-> Maybe DataField
-> FromJSON DataField
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: Value -> Parser DataField
parseJSON :: Value -> Parser DataField
$cparseJSONList :: Value -> Parser [DataField]
parseJSONList :: Value -> Parser [DataField]
$comittedField :: Maybe DataField
omittedField :: Maybe DataField
FromJSON)

data DataCtor = DCtor
  { DataCtor -> LocSymbol
dcName   :: !LocSymbol        -- ^ Ctor Name
  , DataCtor -> [DataField]
dcFields :: ![DataField]      -- ^ Ctor Fields
  } deriving (DataCtor -> DataCtor -> Bool
(DataCtor -> DataCtor -> Bool)
-> (DataCtor -> DataCtor -> Bool) -> Eq DataCtor
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DataCtor -> DataCtor -> Bool
== :: DataCtor -> DataCtor -> Bool
$c/= :: DataCtor -> DataCtor -> Bool
/= :: DataCtor -> DataCtor -> Bool
Eq, Eq DataCtor
Eq DataCtor =>
(DataCtor -> DataCtor -> Ordering)
-> (DataCtor -> DataCtor -> Bool)
-> (DataCtor -> DataCtor -> Bool)
-> (DataCtor -> DataCtor -> Bool)
-> (DataCtor -> DataCtor -> Bool)
-> (DataCtor -> DataCtor -> DataCtor)
-> (DataCtor -> DataCtor -> DataCtor)
-> Ord DataCtor
DataCtor -> DataCtor -> Bool
DataCtor -> DataCtor -> Ordering
DataCtor -> DataCtor -> DataCtor
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: DataCtor -> DataCtor -> Ordering
compare :: DataCtor -> DataCtor -> Ordering
$c< :: DataCtor -> DataCtor -> Bool
< :: DataCtor -> DataCtor -> Bool
$c<= :: DataCtor -> DataCtor -> Bool
<= :: DataCtor -> DataCtor -> Bool
$c> :: DataCtor -> DataCtor -> Bool
> :: DataCtor -> DataCtor -> Bool
$c>= :: DataCtor -> DataCtor -> Bool
>= :: DataCtor -> DataCtor -> Bool
$cmax :: DataCtor -> DataCtor -> DataCtor
max :: DataCtor -> DataCtor -> DataCtor
$cmin :: DataCtor -> DataCtor -> DataCtor
min :: DataCtor -> DataCtor -> DataCtor
Ord, Int -> DataCtor -> ShowS
[DataCtor] -> ShowS
DataCtor -> String
(Int -> DataCtor -> ShowS)
-> (DataCtor -> String) -> ([DataCtor] -> ShowS) -> Show DataCtor
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DataCtor -> ShowS
showsPrec :: Int -> DataCtor -> ShowS
$cshow :: DataCtor -> String
show :: DataCtor -> String
$cshowList :: [DataCtor] -> ShowS
showList :: [DataCtor] -> ShowS
Show, Typeable DataCtor
Typeable DataCtor =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> DataCtor -> c DataCtor)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DataCtor)
-> (DataCtor -> Constr)
-> (DataCtor -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DataCtor))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataCtor))
-> ((forall b. Data b => b -> b) -> DataCtor -> DataCtor)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DataCtor -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DataCtor -> r)
-> (forall u. (forall d. Data d => d -> u) -> DataCtor -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> DataCtor -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> DataCtor -> m DataCtor)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DataCtor -> m DataCtor)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DataCtor -> m DataCtor)
-> Data DataCtor
DataCtor -> Constr
DataCtor -> DataType
(forall b. Data b => b -> b) -> DataCtor -> DataCtor
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> DataCtor -> u
forall u. (forall d. Data d => d -> u) -> DataCtor -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataCtor -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataCtor -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataCtor -> m DataCtor
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataCtor -> m DataCtor
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataCtor
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataCtor -> c DataCtor
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataCtor)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataCtor)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataCtor -> c DataCtor
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataCtor -> c DataCtor
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataCtor
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataCtor
$ctoConstr :: DataCtor -> Constr
toConstr :: DataCtor -> Constr
$cdataTypeOf :: DataCtor -> DataType
dataTypeOf :: DataCtor -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataCtor)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataCtor)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataCtor)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataCtor)
$cgmapT :: (forall b. Data b => b -> b) -> DataCtor -> DataCtor
gmapT :: (forall b. Data b => b -> b) -> DataCtor -> DataCtor
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataCtor -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataCtor -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataCtor -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataCtor -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DataCtor -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> DataCtor -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataCtor -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataCtor -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataCtor -> m DataCtor
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataCtor -> m DataCtor
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataCtor -> m DataCtor
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataCtor -> m DataCtor
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataCtor -> m DataCtor
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataCtor -> m DataCtor
Data, Typeable, (forall x. DataCtor -> Rep DataCtor x)
-> (forall x. Rep DataCtor x -> DataCtor) -> Generic DataCtor
forall x. Rep DataCtor x -> DataCtor
forall x. DataCtor -> Rep DataCtor x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DataCtor -> Rep DataCtor x
from :: forall x. DataCtor -> Rep DataCtor x
$cto :: forall x. Rep DataCtor x -> DataCtor
to :: forall x. Rep DataCtor x -> DataCtor
Generic, [DataCtor] -> Value
[DataCtor] -> Encoding
DataCtor -> Bool
DataCtor -> Value
DataCtor -> Encoding
(DataCtor -> Value)
-> (DataCtor -> Encoding)
-> ([DataCtor] -> Value)
-> ([DataCtor] -> Encoding)
-> (DataCtor -> Bool)
-> ToJSON DataCtor
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: DataCtor -> Value
toJSON :: DataCtor -> Value
$ctoEncoding :: DataCtor -> Encoding
toEncoding :: DataCtor -> Encoding
$ctoJSONList :: [DataCtor] -> Value
toJSONList :: [DataCtor] -> Value
$ctoEncodingList :: [DataCtor] -> Encoding
toEncodingList :: [DataCtor] -> Encoding
$comitField :: DataCtor -> Bool
omitField :: DataCtor -> Bool
ToJSON, Maybe DataCtor
Value -> Parser [DataCtor]
Value -> Parser DataCtor
(Value -> Parser DataCtor)
-> (Value -> Parser [DataCtor])
-> Maybe DataCtor
-> FromJSON DataCtor
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: Value -> Parser DataCtor
parseJSON :: Value -> Parser DataCtor
$cparseJSONList :: Value -> Parser [DataCtor]
parseJSONList :: Value -> Parser [DataCtor]
$comittedField :: Maybe DataCtor
omittedField :: Maybe DataCtor
FromJSON)

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

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

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

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

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

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

    mapSortDataDecl :: (Sort -> Sort) -> DataDecl -> DataDecl
mapSortDataDecl Sort -> Sort
f  DataDecl
dd = DataDecl
dd { ddCtors  = mapSortDataCTor f  <$> ddCtors  dd }
    mapSortDataCTor :: (Sort -> Sort) -> DataCtor -> DataCtor
mapSortDataCTor Sort -> Sort
f  DataCtor
ct = DataCtor
ct { dcFields = mapSortDataField f <$> dcFields ct }
    mapSortDataField :: (Sort -> Sort) -> DataField -> DataField
mapSortDataField Sort -> Sort
f DataField
df = DataField
df { dfSort   = f $ dfSort df }


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

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

isBool :: Sort -> Bool
isBool :: Sort -> Bool
isBool (FTC (TC LocSymbol
c TCInfo
_)) = LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
c Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
boolLConName
isBool 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

isSet :: Sort -> Bool
isSet :: Sort -> Bool
isSet (FTC FTycon
c) = FTycon -> Bool
isSetTC FTycon
c
isSet Sort
_       = Bool
False

isMap :: Sort -> Bool
isMap :: Sort -> Bool
isMap (FTC FTycon
c) = FTycon -> Bool
isMapTC FTycon
c
isMap Sort
_       = Bool
False

isBag :: Sort -> Bool
isBag :: Sort -> Bool
isBag (FTC FTycon
c) = FTycon -> Bool
isBagTC FTycon
c
isBag Sort
_       = Bool
False

isArray :: Sort -> Bool
isArray :: Sort -> Bool
isArray (FTC FTycon
c) = FTycon -> Bool
isArrayTC FTycon
c
isArray Sort
_       = Bool
False

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

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

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

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

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

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

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

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

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

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


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

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

instance Hashable Sort

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

bagSort :: Sort -> Sort
bagSort :: Sort -> Sort
bagSort = Sort -> Sort -> Sort
FApp (FTycon -> Sort
FTC FTycon
bagFTyCon)

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

arraySort :: Sort -> Sort -> Sort
arraySort :: Sort -> Sort -> Sort
arraySort = 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
arrayConName))

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

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

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

type SortSubst = M.HashMap Symbol Sort

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

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

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

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

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

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

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

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


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

instance Hashable TCArgs
instance B.Binary TCArgs

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

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

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

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

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

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

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

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


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

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

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

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

-------------------------------------------------------------------------------
-- | Sort coercion for SMT theory encoding
-------------------------------------------------------------------------------

coerceMapToArray :: Sort -> Sort
coerceMapToArray :: Sort -> Sort
coerceMapToArray (FFunc Sort
sf Sort
sa) = Sort -> Sort -> Sort
FFunc (Sort -> Sort
coerceMapToArray Sort
sf) (Sort -> Sort
coerceMapToArray Sort
sa)
coerceMapToArray (FAbs Int
i Sort
sa)   = Int -> Sort -> Sort
FAbs Int
i (Sort -> Sort
coerceMapToArray Sort
sa)
coerceMapToArray (FApp (FApp Sort
sf Sort
sa) Sort
sb)
  | Sort -> Bool
isMap Sort
sf = Sort -> Sort -> Sort
arraySort (Sort -> Sort
coerceMapToArray Sort
sa) (Sort -> Sort
coerceMapToArray Sort
sb)
  | Bool
otherwise = Sort -> Sort -> Sort
FApp (Sort -> Sort -> Sort
FApp (Sort -> Sort
coerceMapToArray Sort
sf) (Sort -> Sort
coerceMapToArray Sort
sa)) (Sort -> Sort
coerceMapToArray Sort
sb)
coerceMapToArray (FApp Sort
sf Sort
sa) = Sort -> Sort -> Sort
FApp (Sort -> Sort
coerceMapToArray Sort
sf) (Sort -> Sort
coerceMapToArray Sort
sa)
coerceMapToArray Sort
s = Sort
s

coerceSetBagToArray :: Sort -> Sort
coerceSetBagToArray :: Sort -> Sort
coerceSetBagToArray (FFunc Sort
sf Sort
sa) = Sort -> Sort -> Sort
FFunc (Sort -> Sort
coerceSetBagToArray Sort
sf) (Sort -> Sort
coerceSetBagToArray Sort
sa)
coerceSetBagToArray (FAbs Int
i Sort
sa)   = Int -> Sort -> Sort
FAbs Int
i (Sort -> Sort
coerceSetBagToArray Sort
sa)
coerceSetBagToArray (FApp Sort
sf Sort
sa)
  | Sort -> Bool
isSet Sort
sf = Sort -> Sort -> Sort
arraySort (Sort -> Sort
coerceSetBagToArray Sort
sa) Sort
boolSort
  | Sort -> Bool
isBag Sort
sf = Sort -> Sort -> Sort
arraySort (Sort -> Sort
coerceSetBagToArray Sort
sa) Sort
intSort
  | Bool
otherwise = Sort -> Sort -> Sort
FApp (Sort -> Sort
coerceSetBagToArray Sort
sf) (Sort -> Sort
coerceSetBagToArray Sort
sa)
coerceSetBagToArray Sort
s = Sort
s

coerceDataField :: ElabFlags -> DataField -> DataField
coerceDataField :: ElabFlags -> DataField -> DataField
coerceDataField ElabFlags
ef (DField LocSymbol
x Sort
t)  = LocSymbol -> Sort -> DataField
DField LocSymbol
x (((if ElabFlags -> Bool
elabSetBag ElabFlags
ef then Sort -> Sort
coerceSetBagToArray else Sort -> Sort
forall a. a -> a
id) (Sort -> Sort) -> (Sort -> Sort) -> Sort -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Sort
coerceMapToArray) Sort
t)

coerceDataCtor :: ElabFlags -> DataCtor -> DataCtor
coerceDataCtor :: ElabFlags -> DataCtor -> DataCtor
coerceDataCtor ElabFlags
ef (DCtor LocSymbol
x [DataField]
flds) = LocSymbol -> [DataField] -> DataCtor
DCtor LocSymbol
x (ElabFlags -> DataField -> DataField
coerceDataField ElabFlags
ef (DataField -> DataField) -> [DataField] -> [DataField]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataField]
flds)

coerceDataDecl :: ElabFlags -> DataDecl -> DataDecl
coerceDataDecl :: ElabFlags -> DataDecl -> DataDecl
coerceDataDecl ElabFlags
ef (DDecl FTycon
tc Int
n [DataCtor]
ctors) = FTycon -> Int -> [DataCtor] -> DataDecl
DDecl FTycon
tc Int
n (ElabFlags -> DataCtor -> DataCtor
coerceDataCtor ElabFlags
ef (DataCtor -> DataCtor) -> [DataCtor] -> [DataCtor]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCtor]
ctors)