{- |
module: $Header$
description: Higher order logic type operators
license: MIT

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

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

-------------------------------------------------------------------------------
-- Constructors and destructors
-------------------------------------------------------------------------------

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

-------------------------------------------------------------------------------
-- Collecting type operators
-------------------------------------------------------------------------------

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

-------------------------------------------------------------------------------
-- Primitive type operators
-------------------------------------------------------------------------------

-- Booleans

boolName :: Name
boolName :: Name
boolName = String -> Name
mkGlobal String
"bool"

bool :: TypeOp
bool :: TypeOp
bool = Name -> TypeOp
mkUndef Name
boolName

-- Function spaces

funName :: Name
funName :: Name
funName = String -> Name
mkGlobal String
"->"

fun :: TypeOp
fun :: TypeOp
fun = Name -> TypeOp
mkUndef Name
funName

-- Individuals

indName :: Name
indName :: Name
indName = String -> Name
mkGlobal String
"ind"

ind :: TypeOp
ind :: TypeOp
ind = Name -> TypeOp
mkUndef Name
indName

-- All primitive type operators

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]

-------------------------------------------------------------------------------
-- Standard type operators
-------------------------------------------------------------------------------

-- Products

productName :: Name
productName :: Name
productName = Namespace -> String -> Name
Name Namespace
pairNamespace String
"*"

-- Sums

sumName :: Name
sumName :: Name
sumName = Namespace -> String -> Name
Name Namespace
sumNamespace String
"+"

-- Natural numbers

naturalName :: Name
naturalName :: Name
naturalName = Namespace -> String -> Name
Name Namespace
naturalNamespace String
"natural"