{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./HolLight/Term.hs
Description :  Tern for HolLight logic
Copyright   :  (c) Jonathan von Schroeder, DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  jonathan.von_schroeder@dfki.de
Stability   :  experimental
Portability :  portable

Definition of terms for HolLight logic

  Ref.

  <http://www.cl.cam.ac.uk/~jrh13/hol-light/>

-}

module HolLight.Term where

import Data.Data

data HolType = TyVar String | TyApp String [HolType]
  deriving (HolType -> HolType -> Bool
(HolType -> HolType -> Bool)
-> (HolType -> HolType -> Bool) -> Eq HolType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HolType -> HolType -> Bool
$c/= :: HolType -> HolType -> Bool
== :: HolType -> HolType -> Bool
$c== :: HolType -> HolType -> Bool
Eq, Eq HolType
Eq HolType =>
(HolType -> HolType -> Ordering)
-> (HolType -> HolType -> Bool)
-> (HolType -> HolType -> Bool)
-> (HolType -> HolType -> Bool)
-> (HolType -> HolType -> Bool)
-> (HolType -> HolType -> HolType)
-> (HolType -> HolType -> HolType)
-> Ord HolType
HolType -> HolType -> Bool
HolType -> HolType -> Ordering
HolType -> HolType -> HolType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: HolType -> HolType -> HolType
$cmin :: HolType -> HolType -> HolType
max :: HolType -> HolType -> HolType
$cmax :: HolType -> HolType -> HolType
>= :: HolType -> HolType -> Bool
$c>= :: HolType -> HolType -> Bool
> :: HolType -> HolType -> Bool
$c> :: HolType -> HolType -> Bool
<= :: HolType -> HolType -> Bool
$c<= :: HolType -> HolType -> Bool
< :: HolType -> HolType -> Bool
$c< :: HolType -> HolType -> Bool
compare :: HolType -> HolType -> Ordering
$ccompare :: HolType -> HolType -> Ordering
$cp1Ord :: Eq HolType
Ord, Int -> HolType -> ShowS
[HolType] -> ShowS
HolType -> String
(Int -> HolType -> ShowS)
-> (HolType -> String) -> ([HolType] -> ShowS) -> Show HolType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HolType] -> ShowS
$cshowList :: [HolType] -> ShowS
show :: HolType -> String
$cshow :: HolType -> String
showsPrec :: Int -> HolType -> ShowS
$cshowsPrec :: Int -> HolType -> ShowS
Show, ReadPrec [HolType]
ReadPrec HolType
Int -> ReadS HolType
ReadS [HolType]
(Int -> ReadS HolType)
-> ReadS [HolType]
-> ReadPrec HolType
-> ReadPrec [HolType]
-> Read HolType
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [HolType]
$creadListPrec :: ReadPrec [HolType]
readPrec :: ReadPrec HolType
$creadPrec :: ReadPrec HolType
readList :: ReadS [HolType]
$creadList :: ReadS [HolType]
readsPrec :: Int -> ReadS HolType
$creadsPrec :: Int -> ReadS HolType
Read, Typeable, Typeable HolType
Constr
DataType
Typeable HolType =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> HolType -> c HolType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c HolType)
-> (HolType -> Constr)
-> (HolType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c HolType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HolType))
-> ((forall b. Data b => b -> b) -> HolType -> HolType)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> HolType -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> HolType -> r)
-> (forall u. (forall d. Data d => d -> u) -> HolType -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> HolType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> HolType -> m HolType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HolType -> m HolType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HolType -> m HolType)
-> Data HolType
HolType -> Constr
HolType -> DataType
(forall b. Data b => b -> b) -> HolType -> HolType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HolType -> c HolType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HolType
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) -> HolType -> u
forall u. (forall d. Data d => d -> u) -> HolType -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HolType -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HolType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HolType -> m HolType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HolType -> m HolType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HolType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HolType -> c HolType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HolType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HolType)
$cTyApp :: Constr
$cTyVar :: Constr
$tHolType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> HolType -> m HolType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HolType -> m HolType
gmapMp :: (forall d. Data d => d -> m d) -> HolType -> m HolType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HolType -> m HolType
gmapM :: (forall d. Data d => d -> m d) -> HolType -> m HolType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HolType -> m HolType
gmapQi :: Int -> (forall d. Data d => d -> u) -> HolType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> HolType -> u
gmapQ :: (forall d. Data d => d -> u) -> HolType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> HolType -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HolType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HolType -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HolType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HolType -> r
gmapT :: (forall b. Data b => b -> b) -> HolType -> HolType
$cgmapT :: (forall b. Data b => b -> b) -> HolType -> HolType
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HolType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HolType)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c HolType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HolType)
dataTypeOf :: HolType -> DataType
$cdataTypeOf :: HolType -> DataType
toConstr :: HolType -> Constr
$ctoConstr :: HolType -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HolType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HolType
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HolType -> c HolType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HolType -> c HolType
$cp1Data :: Typeable HolType
Data)

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

data HolParseType = Normal | PrefixT
 | InfixL Int | InfixR Int | Binder
 deriving (HolParseType -> HolParseType -> Bool
(HolParseType -> HolParseType -> Bool)
-> (HolParseType -> HolParseType -> Bool) -> Eq HolParseType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HolParseType -> HolParseType -> Bool
$c/= :: HolParseType -> HolParseType -> Bool
== :: HolParseType -> HolParseType -> Bool
$c== :: HolParseType -> HolParseType -> Bool
Eq, Eq HolParseType
Eq HolParseType =>
(HolParseType -> HolParseType -> Ordering)
-> (HolParseType -> HolParseType -> Bool)
-> (HolParseType -> HolParseType -> Bool)
-> (HolParseType -> HolParseType -> Bool)
-> (HolParseType -> HolParseType -> Bool)
-> (HolParseType -> HolParseType -> HolParseType)
-> (HolParseType -> HolParseType -> HolParseType)
-> Ord HolParseType
HolParseType -> HolParseType -> Bool
HolParseType -> HolParseType -> Ordering
HolParseType -> HolParseType -> HolParseType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: HolParseType -> HolParseType -> HolParseType
$cmin :: HolParseType -> HolParseType -> HolParseType
max :: HolParseType -> HolParseType -> HolParseType
$cmax :: HolParseType -> HolParseType -> HolParseType
>= :: HolParseType -> HolParseType -> Bool
$c>= :: HolParseType -> HolParseType -> Bool
> :: HolParseType -> HolParseType -> Bool
$c> :: HolParseType -> HolParseType -> Bool
<= :: HolParseType -> HolParseType -> Bool
$c<= :: HolParseType -> HolParseType -> Bool
< :: HolParseType -> HolParseType -> Bool
$c< :: HolParseType -> HolParseType -> Bool
compare :: HolParseType -> HolParseType -> Ordering
$ccompare :: HolParseType -> HolParseType -> Ordering
$cp1Ord :: Eq HolParseType
Ord, Int -> HolParseType -> ShowS
[HolParseType] -> ShowS
HolParseType -> String
(Int -> HolParseType -> ShowS)
-> (HolParseType -> String)
-> ([HolParseType] -> ShowS)
-> Show HolParseType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HolParseType] -> ShowS
$cshowList :: [HolParseType] -> ShowS
show :: HolParseType -> String
$cshow :: HolParseType -> String
showsPrec :: Int -> HolParseType -> ShowS
$cshowsPrec :: Int -> HolParseType -> ShowS
Show, ReadPrec [HolParseType]
ReadPrec HolParseType
Int -> ReadS HolParseType
ReadS [HolParseType]
(Int -> ReadS HolParseType)
-> ReadS [HolParseType]
-> ReadPrec HolParseType
-> ReadPrec [HolParseType]
-> Read HolParseType
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [HolParseType]
$creadListPrec :: ReadPrec [HolParseType]
readPrec :: ReadPrec HolParseType
$creadPrec :: ReadPrec HolParseType
readList :: ReadS [HolParseType]
$creadList :: ReadS [HolParseType]
readsPrec :: Int -> ReadS HolParseType
$creadsPrec :: Int -> ReadS HolParseType
Read, Typeable, Typeable HolParseType
Constr
DataType
Typeable HolParseType =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> HolParseType -> c HolParseType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c HolParseType)
-> (HolParseType -> Constr)
-> (HolParseType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c HolParseType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c HolParseType))
-> ((forall b. Data b => b -> b) -> HolParseType -> HolParseType)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> HolParseType -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> HolParseType -> r)
-> (forall u. (forall d. Data d => d -> u) -> HolParseType -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> HolParseType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> HolParseType -> m HolParseType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HolParseType -> m HolParseType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HolParseType -> m HolParseType)
-> Data HolParseType
HolParseType -> Constr
HolParseType -> DataType
(forall b. Data b => b -> b) -> HolParseType -> HolParseType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HolParseType -> c HolParseType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HolParseType
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) -> HolParseType -> u
forall u. (forall d. Data d => d -> u) -> HolParseType -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HolParseType -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HolParseType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HolParseType -> m HolParseType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HolParseType -> m HolParseType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HolParseType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HolParseType -> c HolParseType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HolParseType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c HolParseType)
$cBinder :: Constr
$cInfixR :: Constr
$cInfixL :: Constr
$cPrefixT :: Constr
$cNormal :: Constr
$tHolParseType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> HolParseType -> m HolParseType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HolParseType -> m HolParseType
gmapMp :: (forall d. Data d => d -> m d) -> HolParseType -> m HolParseType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HolParseType -> m HolParseType
gmapM :: (forall d. Data d => d -> m d) -> HolParseType -> m HolParseType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HolParseType -> m HolParseType
gmapQi :: Int -> (forall d. Data d => d -> u) -> HolParseType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> HolParseType -> u
gmapQ :: (forall d. Data d => d -> u) -> HolParseType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> HolParseType -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HolParseType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HolParseType -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HolParseType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HolParseType -> r
gmapT :: (forall b. Data b => b -> b) -> HolParseType -> HolParseType
$cgmapT :: (forall b. Data b => b -> b) -> HolParseType -> HolParseType
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c HolParseType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c HolParseType)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c HolParseType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HolParseType)
dataTypeOf :: HolParseType -> DataType
$cdataTypeOf :: HolParseType -> DataType
toConstr :: HolParseType -> Constr
$ctoConstr :: HolParseType -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HolParseType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HolParseType
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HolParseType -> c HolParseType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HolParseType -> c HolParseType
$cp1Data :: Typeable HolParseType
Data)

data HolTermInfo = HolTermInfo (HolParseType, Maybe (String, HolParseType))
  deriving (HolTermInfo -> HolTermInfo -> Bool
(HolTermInfo -> HolTermInfo -> Bool)
-> (HolTermInfo -> HolTermInfo -> Bool) -> Eq HolTermInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HolTermInfo -> HolTermInfo -> Bool
$c/= :: HolTermInfo -> HolTermInfo -> Bool
== :: HolTermInfo -> HolTermInfo -> Bool
$c== :: HolTermInfo -> HolTermInfo -> Bool
Eq, Eq HolTermInfo
Eq HolTermInfo =>
(HolTermInfo -> HolTermInfo -> Ordering)
-> (HolTermInfo -> HolTermInfo -> Bool)
-> (HolTermInfo -> HolTermInfo -> Bool)
-> (HolTermInfo -> HolTermInfo -> Bool)
-> (HolTermInfo -> HolTermInfo -> Bool)
-> (HolTermInfo -> HolTermInfo -> HolTermInfo)
-> (HolTermInfo -> HolTermInfo -> HolTermInfo)
-> Ord HolTermInfo
HolTermInfo -> HolTermInfo -> Bool
HolTermInfo -> HolTermInfo -> Ordering
HolTermInfo -> HolTermInfo -> HolTermInfo
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: HolTermInfo -> HolTermInfo -> HolTermInfo
$cmin :: HolTermInfo -> HolTermInfo -> HolTermInfo
max :: HolTermInfo -> HolTermInfo -> HolTermInfo
$cmax :: HolTermInfo -> HolTermInfo -> HolTermInfo
>= :: HolTermInfo -> HolTermInfo -> Bool
$c>= :: HolTermInfo -> HolTermInfo -> Bool
> :: HolTermInfo -> HolTermInfo -> Bool
$c> :: HolTermInfo -> HolTermInfo -> Bool
<= :: HolTermInfo -> HolTermInfo -> Bool
$c<= :: HolTermInfo -> HolTermInfo -> Bool
< :: HolTermInfo -> HolTermInfo -> Bool
$c< :: HolTermInfo -> HolTermInfo -> Bool
compare :: HolTermInfo -> HolTermInfo -> Ordering
$ccompare :: HolTermInfo -> HolTermInfo -> Ordering
$cp1Ord :: Eq HolTermInfo
Ord, Int -> HolTermInfo -> ShowS
[HolTermInfo] -> ShowS
HolTermInfo -> String
(Int -> HolTermInfo -> ShowS)
-> (HolTermInfo -> String)
-> ([HolTermInfo] -> ShowS)
-> Show HolTermInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HolTermInfo] -> ShowS
$cshowList :: [HolTermInfo] -> ShowS
show :: HolTermInfo -> String
$cshow :: HolTermInfo -> String
showsPrec :: Int -> HolTermInfo -> ShowS
$cshowsPrec :: Int -> HolTermInfo -> ShowS
Show, ReadPrec [HolTermInfo]
ReadPrec HolTermInfo
Int -> ReadS HolTermInfo
ReadS [HolTermInfo]
(Int -> ReadS HolTermInfo)
-> ReadS [HolTermInfo]
-> ReadPrec HolTermInfo
-> ReadPrec [HolTermInfo]
-> Read HolTermInfo
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [HolTermInfo]
$creadListPrec :: ReadPrec [HolTermInfo]
readPrec :: ReadPrec HolTermInfo
$creadPrec :: ReadPrec HolTermInfo
readList :: ReadS [HolTermInfo]
$creadList :: ReadS [HolTermInfo]
readsPrec :: Int -> ReadS HolTermInfo
$creadsPrec :: Int -> ReadS HolTermInfo
Read, Typeable, Typeable HolTermInfo
Constr
DataType
Typeable HolTermInfo =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> HolTermInfo -> c HolTermInfo)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c HolTermInfo)
-> (HolTermInfo -> Constr)
-> (HolTermInfo -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c HolTermInfo))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c HolTermInfo))
-> ((forall b. Data b => b -> b) -> HolTermInfo -> HolTermInfo)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> HolTermInfo -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> HolTermInfo -> r)
-> (forall u. (forall d. Data d => d -> u) -> HolTermInfo -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> HolTermInfo -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> HolTermInfo -> m HolTermInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HolTermInfo -> m HolTermInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HolTermInfo -> m HolTermInfo)
-> Data HolTermInfo
HolTermInfo -> Constr
HolTermInfo -> DataType
(forall b. Data b => b -> b) -> HolTermInfo -> HolTermInfo
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HolTermInfo -> c HolTermInfo
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HolTermInfo
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) -> HolTermInfo -> u
forall u. (forall d. Data d => d -> u) -> HolTermInfo -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HolTermInfo -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HolTermInfo -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HolTermInfo -> m HolTermInfo
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HolTermInfo -> m HolTermInfo
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HolTermInfo
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HolTermInfo -> c HolTermInfo
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HolTermInfo)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c HolTermInfo)
$cHolTermInfo :: Constr
$tHolTermInfo :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> HolTermInfo -> m HolTermInfo
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HolTermInfo -> m HolTermInfo
gmapMp :: (forall d. Data d => d -> m d) -> HolTermInfo -> m HolTermInfo
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HolTermInfo -> m HolTermInfo
gmapM :: (forall d. Data d => d -> m d) -> HolTermInfo -> m HolTermInfo
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HolTermInfo -> m HolTermInfo
gmapQi :: Int -> (forall d. Data d => d -> u) -> HolTermInfo -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> HolTermInfo -> u
gmapQ :: (forall d. Data d => d -> u) -> HolTermInfo -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> HolTermInfo -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HolTermInfo -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HolTermInfo -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HolTermInfo -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HolTermInfo -> r
gmapT :: (forall b. Data b => b -> b) -> HolTermInfo -> HolTermInfo
$cgmapT :: (forall b. Data b => b -> b) -> HolTermInfo -> HolTermInfo
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c HolTermInfo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c HolTermInfo)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c HolTermInfo)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HolTermInfo)
dataTypeOf :: HolTermInfo -> DataType
$cdataTypeOf :: HolTermInfo -> DataType
toConstr :: HolTermInfo -> Constr
$ctoConstr :: HolTermInfo -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HolTermInfo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HolTermInfo
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HolTermInfo -> c HolTermInfo
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HolTermInfo -> c HolTermInfo
$cp1Data :: Typeable HolTermInfo
Data)

data Term = Var String HolType HolTermInfo
     | Const String HolType HolTermInfo
     | Comb Term Term
     | Abs Term Term deriving (Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c== :: Term -> Term -> Bool
Eq, Eq Term
Eq Term =>
(Term -> Term -> Ordering)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Term)
-> (Term -> Term -> Term)
-> Ord Term
Term -> Term -> Bool
Term -> Term -> Ordering
Term -> Term -> Term
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmax :: Term -> Term -> Term
>= :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c< :: Term -> Term -> Bool
compare :: Term -> Term -> Ordering
$ccompare :: Term -> Term -> Ordering
$cp1Ord :: Eq Term
Ord, Int -> Term -> ShowS
[Term] -> ShowS
Term -> String
(Int -> Term -> ShowS)
-> (Term -> String) -> ([Term] -> ShowS) -> Show Term
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Term] -> ShowS
$cshowList :: [Term] -> ShowS
show :: Term -> String
$cshow :: Term -> String
showsPrec :: Int -> Term -> ShowS
$cshowsPrec :: Int -> Term -> ShowS
Show, ReadPrec [Term]
ReadPrec Term
Int -> ReadS Term
ReadS [Term]
(Int -> ReadS Term)
-> ReadS [Term] -> ReadPrec Term -> ReadPrec [Term] -> Read Term
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Term]
$creadListPrec :: ReadPrec [Term]
readPrec :: ReadPrec Term
$creadPrec :: ReadPrec Term
readList :: ReadS [Term]
$creadList :: ReadS [Term]
readsPrec :: Int -> ReadS Term
$creadsPrec :: Int -> ReadS Term
Read, Typeable, Typeable Term
Constr
DataType
Typeable Term =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Term -> c Term)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Term)
-> (Term -> Constr)
-> (Term -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Term))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term))
-> ((forall b. Data b => b -> b) -> Term -> Term)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r)
-> (forall u. (forall d. Data d => d -> u) -> Term -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Term -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Term -> m Term)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Term -> m Term)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Term -> m Term)
-> Data Term
Term -> Constr
Term -> DataType
(forall b. Data b => b -> b) -> Term -> Term
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term -> c Term
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Term
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) -> Term -> u
forall u. (forall d. Data d => d -> u) -> Term -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Term -> m Term
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Term
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term -> c Term
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Term)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)
$cAbs :: Constr
$cComb :: Constr
$cConst :: Constr
$cVar :: Constr
$tTerm :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Term -> m Term
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
gmapMp :: (forall d. Data d => d -> m d) -> Term -> m Term
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
gmapM :: (forall d. Data d => d -> m d) -> Term -> m Term
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Term -> m Term
gmapQi :: Int -> (forall d. Data d => d -> u) -> Term -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Term -> u
gmapQ :: (forall d. Data d => d -> u) -> Term -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Term -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
gmapT :: (forall b. Data b => b -> b) -> Term -> Term
$cgmapT :: (forall b. Data b => b -> b) -> Term -> Term
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Term)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Term)
dataTypeOf :: Term -> DataType
$cdataTypeOf :: Term -> DataType
toConstr :: Term -> Constr
$ctoConstr :: Term -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Term
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Term
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term -> c Term
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term -> c Term
$cp1Data :: Typeable Term
Data)