{- |
module: $Header$
description: Datatypes for higher order logic types and terms
license: MIT

maintainer: Joe Leslie-Hurd <joe@gilith.com>
stability: provisional
portability: portable
-}

module HOL.Data
where

import Data.Set (Set)
import System.Mem.StableName (StableName)

import HOL.Name

-------------------------------------------------------------------------------
-- Size of types and terms
-------------------------------------------------------------------------------

type Size = Integer

-------------------------------------------------------------------------------
-- Type variables
-------------------------------------------------------------------------------

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)

-------------------------------------------------------------------------------
-- Type operators
-------------------------------------------------------------------------------

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)

-------------------------------------------------------------------------------
-- Types
-------------------------------------------------------------------------------

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

-------------------------------------------------------------------------------
-- Variables
-------------------------------------------------------------------------------

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)

-------------------------------------------------------------------------------
-- Constants
-------------------------------------------------------------------------------

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)

-------------------------------------------------------------------------------
-- Terms
-------------------------------------------------------------------------------

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