module HOL.TypeOp
where
import qualified Data.Foldable as Foldable
import Data.Set (Set)
import qualified Data.Set as Set
import HOL.Name
import HOL.Data
name :: TypeOp -> Name
name (TypeOp n _) = n
prov :: TypeOp -> TypeOpProv
prov (TypeOp _ p) = p
mkUndef :: Name -> TypeOp
mkUndef n = TypeOp n UndefTypeOpProv
isUndef :: TypeOp -> Bool
isUndef (TypeOp _ p) = p == UndefTypeOpProv
class HasOps a where
ops :: a -> Set TypeOp
instance HasOps TypeOp where
ops = Set.singleton
instance HasOps a => HasOps [a] where
ops = Foldable.foldMap ops
instance HasOps a => HasOps (Set a) where
ops = Foldable.foldMap ops
instance HasOps TypeData where
ops (VarType _) = Set.empty
ops (OpType t tys) = Set.union (ops t) (ops tys)
instance HasOps Type where
ops (Type d _ _ _) = ops d
instance HasOps Var where
ops (Var _ ty) = ops ty
instance HasOps TermData where
ops (ConstTerm _ ty) = ops ty
ops (VarTerm v) = ops v
ops (AppTerm f x) = Set.union (ops f) (ops x)
ops (AbsTerm v b) = Set.union (ops v) (ops b)
instance HasOps Term where
ops (Term d _ _ _ _ _) = ops d
boolName :: Name
boolName = mkGlobal "bool"
bool :: TypeOp
bool = mkUndef boolName
funName :: Name
funName = mkGlobal "->"
fun :: TypeOp
fun = mkUndef funName
indName :: Name
indName = mkGlobal "ind"
ind :: TypeOp
ind = mkUndef indName
primitives :: Set TypeOp
primitives = Set.fromList [bool,fun,ind]
productName :: Name
productName = Name pairNamespace "*"
sumName :: Name
sumName = Name sumNamespace "+"
naturalName :: Name
naturalName = Name naturalNamespace "natural"