module HOL.Data
where
import Data.Set (Set)
import System.Mem.StableName (StableName)
import HOL.Name
type Size = Integer
data TypeVar =
TypeVar Name
deriving (TypeVar -> TypeVar -> Bool
(TypeVar -> TypeVar -> Bool)
-> (TypeVar -> TypeVar -> Bool) -> Eq TypeVar
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeVar -> TypeVar -> Bool
$c/= :: TypeVar -> TypeVar -> Bool
== :: TypeVar -> TypeVar -> Bool
$c== :: TypeVar -> TypeVar -> Bool
Eq,Eq TypeVar
Eq TypeVar
-> (TypeVar -> TypeVar -> Ordering)
-> (TypeVar -> TypeVar -> Bool)
-> (TypeVar -> TypeVar -> Bool)
-> (TypeVar -> TypeVar -> Bool)
-> (TypeVar -> TypeVar -> Bool)
-> (TypeVar -> TypeVar -> TypeVar)
-> (TypeVar -> TypeVar -> TypeVar)
-> Ord TypeVar
TypeVar -> TypeVar -> Bool
TypeVar -> TypeVar -> Ordering
TypeVar -> TypeVar -> TypeVar
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 :: TypeVar -> TypeVar -> TypeVar
$cmin :: TypeVar -> TypeVar -> TypeVar
max :: TypeVar -> TypeVar -> TypeVar
$cmax :: TypeVar -> TypeVar -> TypeVar
>= :: TypeVar -> TypeVar -> Bool
$c>= :: TypeVar -> TypeVar -> Bool
> :: TypeVar -> TypeVar -> Bool
$c> :: TypeVar -> TypeVar -> Bool
<= :: TypeVar -> TypeVar -> Bool
$c<= :: TypeVar -> TypeVar -> Bool
< :: TypeVar -> TypeVar -> Bool
$c< :: TypeVar -> TypeVar -> Bool
compare :: TypeVar -> TypeVar -> Ordering
$ccompare :: TypeVar -> TypeVar -> Ordering
$cp1Ord :: Eq TypeVar
Ord,Int -> TypeVar -> ShowS
[TypeVar] -> ShowS
TypeVar -> String
(Int -> TypeVar -> ShowS)
-> (TypeVar -> String) -> ([TypeVar] -> ShowS) -> Show TypeVar
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeVar] -> ShowS
$cshowList :: [TypeVar] -> ShowS
show :: TypeVar -> String
$cshow :: TypeVar -> String
showsPrec :: Int -> TypeVar -> ShowS
$cshowsPrec :: Int -> TypeVar -> ShowS
Show)
data TypeOp =
TypeOp Name TypeOpProv
deriving (TypeOp -> TypeOp -> Bool
(TypeOp -> TypeOp -> Bool)
-> (TypeOp -> TypeOp -> Bool) -> Eq TypeOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeOp -> TypeOp -> Bool
$c/= :: TypeOp -> TypeOp -> Bool
== :: TypeOp -> TypeOp -> Bool
$c== :: TypeOp -> TypeOp -> Bool
Eq,Eq TypeOp
Eq TypeOp
-> (TypeOp -> TypeOp -> Ordering)
-> (TypeOp -> TypeOp -> Bool)
-> (TypeOp -> TypeOp -> Bool)
-> (TypeOp -> TypeOp -> Bool)
-> (TypeOp -> TypeOp -> Bool)
-> (TypeOp -> TypeOp -> TypeOp)
-> (TypeOp -> TypeOp -> TypeOp)
-> Ord TypeOp
TypeOp -> TypeOp -> Bool
TypeOp -> TypeOp -> Ordering
TypeOp -> TypeOp -> TypeOp
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 :: TypeOp -> TypeOp -> TypeOp
$cmin :: TypeOp -> TypeOp -> TypeOp
max :: TypeOp -> TypeOp -> TypeOp
$cmax :: TypeOp -> TypeOp -> TypeOp
>= :: TypeOp -> TypeOp -> Bool
$c>= :: TypeOp -> TypeOp -> Bool
> :: TypeOp -> TypeOp -> Bool
$c> :: TypeOp -> TypeOp -> Bool
<= :: TypeOp -> TypeOp -> Bool
$c<= :: TypeOp -> TypeOp -> Bool
< :: TypeOp -> TypeOp -> Bool
$c< :: TypeOp -> TypeOp -> Bool
compare :: TypeOp -> TypeOp -> Ordering
$ccompare :: TypeOp -> TypeOp -> Ordering
$cp1Ord :: Eq TypeOp
Ord,Int -> TypeOp -> ShowS
[TypeOp] -> ShowS
TypeOp -> String
(Int -> TypeOp -> ShowS)
-> (TypeOp -> String) -> ([TypeOp] -> ShowS) -> Show TypeOp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeOp] -> ShowS
$cshowList :: [TypeOp] -> ShowS
show :: TypeOp -> String
$cshow :: TypeOp -> String
showsPrec :: Int -> TypeOp -> ShowS
$cshowsPrec :: Int -> TypeOp -> ShowS
Show)
data TypeOpProv =
UndefTypeOpProv
| DefTypeOpProv TypeOpDef
deriving (TypeOpProv -> TypeOpProv -> Bool
(TypeOpProv -> TypeOpProv -> Bool)
-> (TypeOpProv -> TypeOpProv -> Bool) -> Eq TypeOpProv
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeOpProv -> TypeOpProv -> Bool
$c/= :: TypeOpProv -> TypeOpProv -> Bool
== :: TypeOpProv -> TypeOpProv -> Bool
$c== :: TypeOpProv -> TypeOpProv -> Bool
Eq,Eq TypeOpProv
Eq TypeOpProv
-> (TypeOpProv -> TypeOpProv -> Ordering)
-> (TypeOpProv -> TypeOpProv -> Bool)
-> (TypeOpProv -> TypeOpProv -> Bool)
-> (TypeOpProv -> TypeOpProv -> Bool)
-> (TypeOpProv -> TypeOpProv -> Bool)
-> (TypeOpProv -> TypeOpProv -> TypeOpProv)
-> (TypeOpProv -> TypeOpProv -> TypeOpProv)
-> Ord TypeOpProv
TypeOpProv -> TypeOpProv -> Bool
TypeOpProv -> TypeOpProv -> Ordering
TypeOpProv -> TypeOpProv -> TypeOpProv
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 :: TypeOpProv -> TypeOpProv -> TypeOpProv
$cmin :: TypeOpProv -> TypeOpProv -> TypeOpProv
max :: TypeOpProv -> TypeOpProv -> TypeOpProv
$cmax :: TypeOpProv -> TypeOpProv -> TypeOpProv
>= :: TypeOpProv -> TypeOpProv -> Bool
$c>= :: TypeOpProv -> TypeOpProv -> Bool
> :: TypeOpProv -> TypeOpProv -> Bool
$c> :: TypeOpProv -> TypeOpProv -> Bool
<= :: TypeOpProv -> TypeOpProv -> Bool
$c<= :: TypeOpProv -> TypeOpProv -> Bool
< :: TypeOpProv -> TypeOpProv -> Bool
$c< :: TypeOpProv -> TypeOpProv -> Bool
compare :: TypeOpProv -> TypeOpProv -> Ordering
$ccompare :: TypeOpProv -> TypeOpProv -> Ordering
$cp1Ord :: Eq TypeOpProv
Ord,Int -> TypeOpProv -> ShowS
[TypeOpProv] -> ShowS
TypeOpProv -> String
(Int -> TypeOpProv -> ShowS)
-> (TypeOpProv -> String)
-> ([TypeOpProv] -> ShowS)
-> Show TypeOpProv
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeOpProv] -> ShowS
$cshowList :: [TypeOpProv] -> ShowS
show :: TypeOpProv -> String
$cshow :: TypeOpProv -> String
showsPrec :: Int -> TypeOpProv -> ShowS
$cshowsPrec :: Int -> TypeOpProv -> ShowS
Show)
data TypeOpDef =
TypeOpDef Term [TypeVar]
deriving (TypeOpDef -> TypeOpDef -> Bool
(TypeOpDef -> TypeOpDef -> Bool)
-> (TypeOpDef -> TypeOpDef -> Bool) -> Eq TypeOpDef
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeOpDef -> TypeOpDef -> Bool
$c/= :: TypeOpDef -> TypeOpDef -> Bool
== :: TypeOpDef -> TypeOpDef -> Bool
$c== :: TypeOpDef -> TypeOpDef -> Bool
Eq,Eq TypeOpDef
Eq TypeOpDef
-> (TypeOpDef -> TypeOpDef -> Ordering)
-> (TypeOpDef -> TypeOpDef -> Bool)
-> (TypeOpDef -> TypeOpDef -> Bool)
-> (TypeOpDef -> TypeOpDef -> Bool)
-> (TypeOpDef -> TypeOpDef -> Bool)
-> (TypeOpDef -> TypeOpDef -> TypeOpDef)
-> (TypeOpDef -> TypeOpDef -> TypeOpDef)
-> Ord TypeOpDef
TypeOpDef -> TypeOpDef -> Bool
TypeOpDef -> TypeOpDef -> Ordering
TypeOpDef -> TypeOpDef -> TypeOpDef
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 :: TypeOpDef -> TypeOpDef -> TypeOpDef
$cmin :: TypeOpDef -> TypeOpDef -> TypeOpDef
max :: TypeOpDef -> TypeOpDef -> TypeOpDef
$cmax :: TypeOpDef -> TypeOpDef -> TypeOpDef
>= :: TypeOpDef -> TypeOpDef -> Bool
$c>= :: TypeOpDef -> TypeOpDef -> Bool
> :: TypeOpDef -> TypeOpDef -> Bool
$c> :: TypeOpDef -> TypeOpDef -> Bool
<= :: TypeOpDef -> TypeOpDef -> Bool
$c<= :: TypeOpDef -> TypeOpDef -> Bool
< :: TypeOpDef -> TypeOpDef -> Bool
$c< :: TypeOpDef -> TypeOpDef -> Bool
compare :: TypeOpDef -> TypeOpDef -> Ordering
$ccompare :: TypeOpDef -> TypeOpDef -> Ordering
$cp1Ord :: Eq TypeOpDef
Ord,Int -> TypeOpDef -> ShowS
[TypeOpDef] -> ShowS
TypeOpDef -> String
(Int -> TypeOpDef -> ShowS)
-> (TypeOpDef -> String)
-> ([TypeOpDef] -> ShowS)
-> Show TypeOpDef
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeOpDef] -> ShowS
$cshowList :: [TypeOpDef] -> ShowS
show :: TypeOpDef -> String
$cshow :: TypeOpDef -> String
showsPrec :: Int -> TypeOpDef -> ShowS
$cshowsPrec :: Int -> TypeOpDef -> ShowS
Show)
data Type = Type TypeData TypeId Size (Set TypeVar)
data TypeData =
VarType TypeVar
| OpType TypeOp [Type]
deriving (TypeData -> TypeData -> Bool
(TypeData -> TypeData -> Bool)
-> (TypeData -> TypeData -> Bool) -> Eq TypeData
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeData -> TypeData -> Bool
$c/= :: TypeData -> TypeData -> Bool
== :: TypeData -> TypeData -> Bool
$c== :: TypeData -> TypeData -> Bool
Eq,Eq TypeData
Eq TypeData
-> (TypeData -> TypeData -> Ordering)
-> (TypeData -> TypeData -> Bool)
-> (TypeData -> TypeData -> Bool)
-> (TypeData -> TypeData -> Bool)
-> (TypeData -> TypeData -> Bool)
-> (TypeData -> TypeData -> TypeData)
-> (TypeData -> TypeData -> TypeData)
-> Ord TypeData
TypeData -> TypeData -> Bool
TypeData -> TypeData -> Ordering
TypeData -> TypeData -> TypeData
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 :: TypeData -> TypeData -> TypeData
$cmin :: TypeData -> TypeData -> TypeData
max :: TypeData -> TypeData -> TypeData
$cmax :: TypeData -> TypeData -> TypeData
>= :: TypeData -> TypeData -> Bool
$c>= :: TypeData -> TypeData -> Bool
> :: TypeData -> TypeData -> Bool
$c> :: TypeData -> TypeData -> Bool
<= :: TypeData -> TypeData -> Bool
$c<= :: TypeData -> TypeData -> Bool
< :: TypeData -> TypeData -> Bool
$c< :: TypeData -> TypeData -> Bool
compare :: TypeData -> TypeData -> Ordering
$ccompare :: TypeData -> TypeData -> Ordering
$cp1Ord :: Eq TypeData
Ord,Int -> TypeData -> ShowS
[TypeData] -> ShowS
TypeData -> String
(Int -> TypeData -> ShowS)
-> (TypeData -> String) -> ([TypeData] -> ShowS) -> Show TypeData
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeData] -> ShowS
$cshowList :: [TypeData] -> ShowS
show :: TypeData -> String
$cshow :: TypeData -> String
showsPrec :: Int -> TypeData -> ShowS
$cshowsPrec :: Int -> TypeData -> ShowS
Show)
type TypeId = StableName TypeData
instance Eq Type where
(Type TypeData
d1 TypeId
i1 Size
s1 Set TypeVar
_) == :: Type -> Type -> Bool
== (Type TypeData
d2 TypeId
i2 Size
s2 Set TypeVar
_) =
Size
s1 Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
s2 Bool -> Bool -> Bool
&& (TypeId
i1 TypeId -> TypeId -> Bool
forall a. Eq a => a -> a -> Bool
== TypeId
i2 Bool -> Bool -> Bool
|| TypeData
d1 TypeData -> TypeData -> Bool
forall a. Eq a => a -> a -> Bool
== TypeData
d2)
instance Ord Type where
compare :: Type -> Type -> Ordering
compare (Type TypeData
d1 TypeId
i1 Size
s1 Set TypeVar
_) (Type TypeData
d2 TypeId
i2 Size
s2 Set TypeVar
_) =
case Size -> Size -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Size
s1 Size
s2 of
Ordering
EQ -> if TypeId
i1 TypeId -> TypeId -> Bool
forall a. Eq a => a -> a -> Bool
== TypeId
i2 then Ordering
EQ else TypeData -> TypeData -> Ordering
forall a. Ord a => a -> a -> Ordering
compare TypeData
d1 TypeData
d2
Ordering
x -> Ordering
x
instance Show Type where
show :: Type -> String
show (Type TypeData
_ TypeId
_ Size
s Set TypeVar
_) = ShowS
forall a. Show a => a -> String
show ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"Type<" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Size -> String
forall a. Show a => a -> String
show Size
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"
data Var =
Var Name Type
deriving (Var -> Var -> Bool
(Var -> Var -> Bool) -> (Var -> Var -> Bool) -> Eq Var
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c== :: Var -> Var -> Bool
Eq,Eq Var
Eq Var
-> (Var -> Var -> Ordering)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Var)
-> (Var -> Var -> Var)
-> Ord Var
Var -> Var -> Bool
Var -> Var -> Ordering
Var -> Var -> Var
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 :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmax :: Var -> Var -> Var
>= :: Var -> Var -> Bool
$c>= :: Var -> Var -> Bool
> :: Var -> Var -> Bool
$c> :: Var -> Var -> Bool
<= :: Var -> Var -> Bool
$c<= :: Var -> Var -> Bool
< :: Var -> Var -> Bool
$c< :: Var -> Var -> Bool
compare :: Var -> Var -> Ordering
$ccompare :: Var -> Var -> Ordering
$cp1Ord :: Eq Var
Ord,Int -> Var -> ShowS
[Var] -> ShowS
Var -> String
(Int -> Var -> ShowS)
-> (Var -> String) -> ([Var] -> ShowS) -> Show Var
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Var] -> ShowS
$cshowList :: [Var] -> ShowS
show :: Var -> String
$cshow :: Var -> String
showsPrec :: Int -> Var -> ShowS
$cshowsPrec :: Int -> Var -> ShowS
Show)
data Const =
Const Name ConstProv
deriving (Const -> Const -> Bool
(Const -> Const -> Bool) -> (Const -> Const -> Bool) -> Eq Const
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Const -> Const -> Bool
$c/= :: Const -> Const -> Bool
== :: Const -> Const -> Bool
$c== :: Const -> Const -> Bool
Eq,Eq Const
Eq Const
-> (Const -> Const -> Ordering)
-> (Const -> Const -> Bool)
-> (Const -> Const -> Bool)
-> (Const -> Const -> Bool)
-> (Const -> Const -> Bool)
-> (Const -> Const -> Const)
-> (Const -> Const -> Const)
-> Ord Const
Const -> Const -> Bool
Const -> Const -> Ordering
Const -> Const -> Const
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 :: Const -> Const -> Const
$cmin :: Const -> Const -> Const
max :: Const -> Const -> Const
$cmax :: Const -> Const -> Const
>= :: Const -> Const -> Bool
$c>= :: Const -> Const -> Bool
> :: Const -> Const -> Bool
$c> :: Const -> Const -> Bool
<= :: Const -> Const -> Bool
$c<= :: Const -> Const -> Bool
< :: Const -> Const -> Bool
$c< :: Const -> Const -> Bool
compare :: Const -> Const -> Ordering
$ccompare :: Const -> Const -> Ordering
$cp1Ord :: Eq Const
Ord,Int -> Const -> ShowS
[Const] -> ShowS
Const -> String
(Int -> Const -> ShowS)
-> (Const -> String) -> ([Const] -> ShowS) -> Show Const
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Const] -> ShowS
$cshowList :: [Const] -> ShowS
show :: Const -> String
$cshow :: Const -> String
showsPrec :: Int -> Const -> ShowS
$cshowsPrec :: Int -> Const -> ShowS
Show)
data ConstProv =
UndefConstProv
| DefConstProv ConstDef
| AbsConstProv TypeOpDef
| RepConstProv TypeOpDef
deriving (ConstProv -> ConstProv -> Bool
(ConstProv -> ConstProv -> Bool)
-> (ConstProv -> ConstProv -> Bool) -> Eq ConstProv
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConstProv -> ConstProv -> Bool
$c/= :: ConstProv -> ConstProv -> Bool
== :: ConstProv -> ConstProv -> Bool
$c== :: ConstProv -> ConstProv -> Bool
Eq,Eq ConstProv
Eq ConstProv
-> (ConstProv -> ConstProv -> Ordering)
-> (ConstProv -> ConstProv -> Bool)
-> (ConstProv -> ConstProv -> Bool)
-> (ConstProv -> ConstProv -> Bool)
-> (ConstProv -> ConstProv -> Bool)
-> (ConstProv -> ConstProv -> ConstProv)
-> (ConstProv -> ConstProv -> ConstProv)
-> Ord ConstProv
ConstProv -> ConstProv -> Bool
ConstProv -> ConstProv -> Ordering
ConstProv -> ConstProv -> ConstProv
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 :: ConstProv -> ConstProv -> ConstProv
$cmin :: ConstProv -> ConstProv -> ConstProv
max :: ConstProv -> ConstProv -> ConstProv
$cmax :: ConstProv -> ConstProv -> ConstProv
>= :: ConstProv -> ConstProv -> Bool
$c>= :: ConstProv -> ConstProv -> Bool
> :: ConstProv -> ConstProv -> Bool
$c> :: ConstProv -> ConstProv -> Bool
<= :: ConstProv -> ConstProv -> Bool
$c<= :: ConstProv -> ConstProv -> Bool
< :: ConstProv -> ConstProv -> Bool
$c< :: ConstProv -> ConstProv -> Bool
compare :: ConstProv -> ConstProv -> Ordering
$ccompare :: ConstProv -> ConstProv -> Ordering
$cp1Ord :: Eq ConstProv
Ord,Int -> ConstProv -> ShowS
[ConstProv] -> ShowS
ConstProv -> String
(Int -> ConstProv -> ShowS)
-> (ConstProv -> String)
-> ([ConstProv] -> ShowS)
-> Show ConstProv
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ConstProv] -> ShowS
$cshowList :: [ConstProv] -> ShowS
show :: ConstProv -> String
$cshow :: ConstProv -> String
showsPrec :: Int -> ConstProv -> ShowS
$cshowsPrec :: Int -> ConstProv -> ShowS
Show)
data ConstDef =
ConstDef Term
deriving (ConstDef -> ConstDef -> Bool
(ConstDef -> ConstDef -> Bool)
-> (ConstDef -> ConstDef -> Bool) -> Eq ConstDef
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConstDef -> ConstDef -> Bool
$c/= :: ConstDef -> ConstDef -> Bool
== :: ConstDef -> ConstDef -> Bool
$c== :: ConstDef -> ConstDef -> Bool
Eq,Eq ConstDef
Eq ConstDef
-> (ConstDef -> ConstDef -> Ordering)
-> (ConstDef -> ConstDef -> Bool)
-> (ConstDef -> ConstDef -> Bool)
-> (ConstDef -> ConstDef -> Bool)
-> (ConstDef -> ConstDef -> Bool)
-> (ConstDef -> ConstDef -> ConstDef)
-> (ConstDef -> ConstDef -> ConstDef)
-> Ord ConstDef
ConstDef -> ConstDef -> Bool
ConstDef -> ConstDef -> Ordering
ConstDef -> ConstDef -> ConstDef
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 :: ConstDef -> ConstDef -> ConstDef
$cmin :: ConstDef -> ConstDef -> ConstDef
max :: ConstDef -> ConstDef -> ConstDef
$cmax :: ConstDef -> ConstDef -> ConstDef
>= :: ConstDef -> ConstDef -> Bool
$c>= :: ConstDef -> ConstDef -> Bool
> :: ConstDef -> ConstDef -> Bool
$c> :: ConstDef -> ConstDef -> Bool
<= :: ConstDef -> ConstDef -> Bool
$c<= :: ConstDef -> ConstDef -> Bool
< :: ConstDef -> ConstDef -> Bool
$c< :: ConstDef -> ConstDef -> Bool
compare :: ConstDef -> ConstDef -> Ordering
$ccompare :: ConstDef -> ConstDef -> Ordering
$cp1Ord :: Eq ConstDef
Ord,Int -> ConstDef -> ShowS
[ConstDef] -> ShowS
ConstDef -> String
(Int -> ConstDef -> ShowS)
-> (ConstDef -> String) -> ([ConstDef] -> ShowS) -> Show ConstDef
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ConstDef] -> ShowS
$cshowList :: [ConstDef] -> ShowS
show :: ConstDef -> String
$cshow :: ConstDef -> String
showsPrec :: Int -> ConstDef -> ShowS
$cshowsPrec :: Int -> ConstDef -> ShowS
Show)
data Term = Term TermData TermId Size Type (Set TypeVar) (Set Var)
data TermData =
ConstTerm Const Type
| VarTerm Var
| AppTerm Term Term
| AbsTerm Var Term
deriving (TermData -> TermData -> Bool
(TermData -> TermData -> Bool)
-> (TermData -> TermData -> Bool) -> Eq TermData
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TermData -> TermData -> Bool
$c/= :: TermData -> TermData -> Bool
== :: TermData -> TermData -> Bool
$c== :: TermData -> TermData -> Bool
Eq,Eq TermData
Eq TermData
-> (TermData -> TermData -> Ordering)
-> (TermData -> TermData -> Bool)
-> (TermData -> TermData -> Bool)
-> (TermData -> TermData -> Bool)
-> (TermData -> TermData -> Bool)
-> (TermData -> TermData -> TermData)
-> (TermData -> TermData -> TermData)
-> Ord TermData
TermData -> TermData -> Bool
TermData -> TermData -> Ordering
TermData -> TermData -> TermData
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 :: TermData -> TermData -> TermData
$cmin :: TermData -> TermData -> TermData
max :: TermData -> TermData -> TermData
$cmax :: TermData -> TermData -> TermData
>= :: TermData -> TermData -> Bool
$c>= :: TermData -> TermData -> Bool
> :: TermData -> TermData -> Bool
$c> :: TermData -> TermData -> Bool
<= :: TermData -> TermData -> Bool
$c<= :: TermData -> TermData -> Bool
< :: TermData -> TermData -> Bool
$c< :: TermData -> TermData -> Bool
compare :: TermData -> TermData -> Ordering
$ccompare :: TermData -> TermData -> Ordering
$cp1Ord :: Eq TermData
Ord,Int -> TermData -> ShowS
[TermData] -> ShowS
TermData -> String
(Int -> TermData -> ShowS)
-> (TermData -> String) -> ([TermData] -> ShowS) -> Show TermData
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TermData] -> ShowS
$cshowList :: [TermData] -> ShowS
show :: TermData -> String
$cshow :: TermData -> String
showsPrec :: Int -> TermData -> ShowS
$cshowsPrec :: Int -> TermData -> ShowS
Show)
type TermId = StableName TermData
instance Eq Term where
(Term TermData
d1 TermId
i1 Size
s1 Type
_ Set TypeVar
_ Set Var
_) == :: Term -> Term -> Bool
== (Term TermData
d2 TermId
i2 Size
s2 Type
_ Set TypeVar
_ Set Var
_) =
Size
s1 Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
s2 Bool -> Bool -> Bool
&& (TermId
i1 TermId -> TermId -> Bool
forall a. Eq a => a -> a -> Bool
== TermId
i2 Bool -> Bool -> Bool
|| TermData
d1 TermData -> TermData -> Bool
forall a. Eq a => a -> a -> Bool
== TermData
d2)
instance Ord Term where
compare :: Term -> Term -> Ordering
compare (Term TermData
d1 TermId
i1 Size
s1 Type
_ Set TypeVar
_ Set Var
_) (Term TermData
d2 TermId
i2 Size
s2 Type
_ Set TypeVar
_ Set Var
_) =
case Size -> Size -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Size
s1 Size
s2 of
Ordering
EQ -> if TermId
i1 TermId -> TermId -> Bool
forall a. Eq a => a -> a -> Bool
== TermId
i2 then Ordering
EQ else TermData -> TermData -> Ordering
forall a. Ord a => a -> a -> Ordering
compare TermData
d1 TermData
d2
Ordering
x -> Ordering
x
instance Show Term where
show :: Term -> String
show (Term TermData
_ TermId
_ Size
s Type
_ Set TypeVar
_ Set Var
_) = ShowS
forall a. Show a => a -> String
show ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"Term<" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Size -> String
forall a. Show a => a -> String
show Size
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"