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 -> Name
name (TypeOp Name
n TypeOpProv
_) = Name
n
prov :: TypeOp -> TypeOpProv
prov :: TypeOp -> TypeOpProv
prov (TypeOp Name
_ TypeOpProv
p) = TypeOpProv
p
mkUndef :: Name -> TypeOp
mkUndef :: Name -> TypeOp
mkUndef Name
n = Name -> TypeOpProv -> TypeOp
TypeOp Name
n TypeOpProv
UndefTypeOpProv
isUndef :: TypeOp -> Bool
isUndef :: TypeOp -> Bool
isUndef (TypeOp Name
_ TypeOpProv
p) = TypeOpProv
p TypeOpProv -> TypeOpProv -> Bool
forall a. Eq a => a -> a -> Bool
== TypeOpProv
UndefTypeOpProv
class HasOps a where
ops :: a -> Set TypeOp
instance HasOps TypeOp where
ops :: TypeOp -> Set TypeOp
ops = TypeOp -> Set TypeOp
forall a. a -> Set a
Set.singleton
instance HasOps a => HasOps [a] where
ops :: [a] -> Set TypeOp
ops = (a -> Set TypeOp) -> [a] -> Set TypeOp
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Foldable.foldMap a -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
ops
instance HasOps a => HasOps (Set a) where
ops :: Set a -> Set TypeOp
ops = (a -> Set TypeOp) -> Set a -> Set TypeOp
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Foldable.foldMap a -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
ops
instance HasOps TypeData where
ops :: TypeData -> Set TypeOp
ops (VarType TypeVar
_) = Set TypeOp
forall a. Set a
Set.empty
ops (OpType TypeOp
t [Type]
tys) = Set TypeOp -> Set TypeOp -> Set TypeOp
forall a. Ord a => Set a -> Set a -> Set a
Set.union (TypeOp -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
ops TypeOp
t) ([Type] -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
ops [Type]
tys)
instance HasOps Type where
ops :: Type -> Set TypeOp
ops (Type TypeData
d TypeId
_ Size
_ Set TypeVar
_) = TypeData -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
ops TypeData
d
instance HasOps Var where
ops :: Var -> Set TypeOp
ops (Var Name
_ Type
ty) = Type -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
ops Type
ty
instance HasOps TermData where
ops :: TermData -> Set TypeOp
ops (ConstTerm Const
_ Type
ty) = Type -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
ops Type
ty
ops (VarTerm Var
v) = Var -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
ops Var
v
ops (AppTerm Term
f Term
x) = Set TypeOp -> Set TypeOp -> Set TypeOp
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Term -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
ops Term
f) (Term -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
ops Term
x)
ops (AbsTerm Var
v Term
b) = Set TypeOp -> Set TypeOp -> Set TypeOp
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Var -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
ops Var
v) (Term -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
ops Term
b)
instance HasOps Term where
ops :: Term -> Set TypeOp
ops (Term TermData
d TermId
_ Size
_ Type
_ Set TypeVar
_ Set Var
_) = TermData -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
ops TermData
d
boolName :: Name
boolName :: Name
boolName = String -> Name
mkGlobal String
"bool"
bool :: TypeOp
bool :: TypeOp
bool = Name -> TypeOp
mkUndef Name
boolName
funName :: Name
funName :: Name
funName = String -> Name
mkGlobal String
"->"
fun :: TypeOp
fun :: TypeOp
fun = Name -> TypeOp
mkUndef Name
funName
indName :: Name
indName :: Name
indName = String -> Name
mkGlobal String
"ind"
ind :: TypeOp
ind :: TypeOp
ind = Name -> TypeOp
mkUndef Name
indName
primitives :: Set TypeOp
primitives :: Set TypeOp
primitives = [TypeOp] -> Set TypeOp
forall a. Ord a => [a] -> Set a
Set.fromList [TypeOp
bool,TypeOp
fun,TypeOp
ind]
productName :: Name
productName :: Name
productName = Namespace -> String -> Name
Name Namespace
pairNamespace String
"*"
sumName :: Name
sumName :: Name
sumName = Namespace -> String -> Name
Name Namespace
sumNamespace String
"+"
naturalName :: Name
naturalName :: Name
naturalName = Namespace -> String -> Name
Name Namespace
naturalNamespace String
"natural"