module HOL.Data
where
import Data.Set (Set)
import System.Mem.StableName (StableName)
import HOL.Name
type Size = Integer
data TypeVar =
TypeVar Name
deriving (Eq,Ord,Show)
data TypeOp =
TypeOp Name TypeOpProv
deriving (Eq,Ord,Show)
data TypeOpProv =
UndefTypeOpProv
| DefTypeOpProv TypeOpDef
deriving (Eq,Ord,Show)
data TypeOpDef =
TypeOpDef Term [TypeVar]
deriving (Eq,Ord,Show)
data Type = Type TypeData TypeId Size (Set TypeVar)
data TypeData =
VarType TypeVar
| OpType TypeOp [Type]
deriving (Eq,Ord,Show)
type TypeId = StableName TypeData
instance Eq Type where
(Type d1 i1 s1 _) == (Type d2 i2 s2 _) =
s1 == s2 && (i1 == i2 || d1 == d2)
instance Ord Type where
compare (Type d1 i1 s1 _) (Type d2 i2 s2 _) =
case compare s1 s2 of
EQ -> if i1 == i2 then EQ else compare d1 d2
x -> x
instance Show Type where
show (Type _ _ s _) = show $ "Type<" ++ show s ++ ">"
data Var =
Var Name Type
deriving (Eq,Ord,Show)
data Const =
Const Name ConstProv
deriving (Eq,Ord,Show)
data ConstProv =
UndefConstProv
| DefConstProv ConstDef
| AbsConstProv TypeOpDef
| RepConstProv TypeOpDef
deriving (Eq,Ord,Show)
data ConstDef =
ConstDef Term
deriving (Eq,Ord,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 (Eq,Ord,Show)
type TermId = StableName TermData
instance Eq Term where
(Term d1 i1 s1 _ _ _) == (Term d2 i2 s2 _ _ _) =
s1 == s2 && (i1 == i2 || d1 == d2)
instance Ord Term where
compare (Term d1 i1 s1 _ _ _) (Term d2 i2 s2 _ _ _) =
case compare s1 s2 of
EQ -> if i1 == i2 then EQ else compare d1 d2
x -> x
instance Show Term where
show (Term _ _ s _ _ _) = show $ "Term<" ++ show s ++ ">"