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

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

module HOL.Const
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 :: Const -> Name
name :: Const -> Name
name (Const Name
n ConstProv
_) = Name
n

prov :: Const -> ConstProv
prov :: Const -> ConstProv
prov (Const Name
_ ConstProv
p) = ConstProv
p

mkUndef :: Name -> Const
mkUndef :: Name -> Const
mkUndef Name
n = Name -> ConstProv -> Const
Const Name
n ConstProv
UndefConstProv

isUndef :: Const -> Bool
isUndef :: Const -> Bool
isUndef (Const Name
_ ConstProv
p) = ConstProv
p ConstProv -> ConstProv -> Bool
forall a. Eq a => a -> a -> Bool
== ConstProv
UndefConstProv

-------------------------------------------------------------------------------
-- Collecting constants
-------------------------------------------------------------------------------

class HasConsts a where
  consts :: a -> Set Const

instance HasConsts Const where
  consts :: Const -> Set Const
consts = Const -> Set Const
forall a. a -> Set a
Set.singleton

instance HasConsts a => HasConsts [a] where
  consts :: [a] -> Set Const
consts = (a -> Set Const) -> [a] -> Set Const
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Foldable.foldMap a -> Set Const
forall a. HasConsts a => a -> Set Const
consts

instance HasConsts a => HasConsts (Set a) where
  consts :: Set a -> Set Const
consts = (a -> Set Const) -> Set a -> Set Const
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Foldable.foldMap a -> Set Const
forall a. HasConsts a => a -> Set Const
consts

instance HasConsts TermData where
  consts :: TermData -> Set Const
consts (ConstTerm Const
c Type
_) = Const -> Set Const
forall a. HasConsts a => a -> Set Const
consts Const
c
  consts (VarTerm Var
_) = Set Const
forall a. Set a
Set.empty
  consts (AppTerm Term
f Term
x) = Set Const -> Set Const -> Set Const
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Term -> Set Const
forall a. HasConsts a => a -> Set Const
consts Term
f) (Term -> Set Const
forall a. HasConsts a => a -> Set Const
consts Term
x)
  consts (AbsTerm Var
_ Term
b) = Term -> Set Const
forall a. HasConsts a => a -> Set Const
consts Term
b

instance HasConsts Term where
  consts :: Term -> Set Const
consts (Term TermData
d TermId
_ Size
_ Type
_ Set TypeVar
_ Set Var
_) = TermData -> Set Const
forall a. HasConsts a => a -> Set Const
consts TermData
d

-------------------------------------------------------------------------------
-- Primitive constants
-------------------------------------------------------------------------------

-- Equality

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

eq :: Const
eq :: Const
eq = Name -> Const
mkUndef Name
eqName

-- Hilbert's indefinite choice operator

selectName :: Name
selectName :: Name
selectName = String -> Name
mkGlobal String
"select"

select :: Const
select :: Const
select = Name -> Const
mkUndef Name
selectName

-- All primitive constants

primitives :: Set Const
primitives :: Set Const
primitives = [Const] -> Set Const
forall a. Ord a => [a] -> Set a
Set.fromList [Const
eq,Const
select]

-------------------------------------------------------------------------------
-- Standard constants
-------------------------------------------------------------------------------

-- Booleans

condName :: Name
condName :: Name
condName = Namespace -> String -> Name
Name Namespace
boolNamespace String
"cond"

conjName :: Name
conjName :: Name
conjName = Namespace -> String -> Name
Name Namespace
boolNamespace String
"/\\"

disjName :: Name
disjName :: Name
disjName = Namespace -> String -> Name
Name Namespace
boolNamespace String
"\\/"

existsName :: Name
existsName :: Name
existsName = Namespace -> String -> Name
Name Namespace
boolNamespace String
"?"

existsUniqueName :: Name
existsUniqueName :: Name
existsUniqueName = Namespace -> String -> Name
Name Namespace
boolNamespace String
"?!"

forallName :: Name
forallName :: Name
forallName = Namespace -> String -> Name
Name Namespace
boolNamespace String
"!"

impName :: Name
impName :: Name
impName = Namespace -> String -> Name
Name Namespace
boolNamespace String
"==>"

negName :: Name
negName :: Name
negName = Namespace -> String -> Name
Name Namespace
boolNamespace String
"~"

-- Lists

appendName :: Name
appendName :: Name
appendName = Namespace -> String -> Name
Name Namespace
listNamespace String
"@"

consName :: Name
consName :: Name
consName = Namespace -> String -> Name
Name Namespace
listNamespace String
"::"

-- Products

pairName :: Name
pairName :: Name
pairName = Namespace -> String -> Name
Name Namespace
pairNamespace String
","

-- Functions

composeName :: Name
composeName :: Name
composeName = Namespace -> String -> Name
Name Namespace
functionNamespace String
"o"

funpowName :: Name
funpowName :: Name
funpowName = Namespace -> String -> Name
Name Namespace
functionNamespace String
"^"

-- Natural numbers

addName :: Name
addName :: Name
addName = Namespace -> String -> Name
Name Namespace
naturalNamespace String
"+"

bit0Name :: Name
bit0Name :: Name
bit0Name = Namespace -> String -> Name
Name Namespace
naturalNamespace String
"bit0"

bit1Name :: Name
bit1Name :: Name
bit1Name = Namespace -> String -> Name
Name Namespace
naturalNamespace String
"bit1"

divName :: Name
divName :: Name
divName = Namespace -> String -> Name
Name Namespace
naturalNamespace String
"div"

geName :: Name
geName :: Name
geName = Namespace -> String -> Name
Name Namespace
naturalNamespace String
">="

gtName :: Name
gtName :: Name
gtName = Namespace -> String -> Name
Name Namespace
naturalNamespace String
">"

leName :: Name
leName :: Name
leName = Namespace -> String -> Name
Name Namespace
naturalNamespace String
"<="

ltName :: Name
ltName :: Name
ltName = Namespace -> String -> Name
Name Namespace
naturalNamespace String
"<"

modName :: Name
modName :: Name
modName = Namespace -> String -> Name
Name Namespace
naturalNamespace String
"mod"

multName :: Name
multName :: Name
multName = Namespace -> String -> Name
Name Namespace
naturalNamespace String
"*"

powerName :: Name
powerName :: Name
powerName = Namespace -> String -> Name
Name Namespace
naturalNamespace String
"^"

subName :: Name
subName :: Name
subName = Namespace -> String -> Name
Name Namespace
naturalNamespace String
"-"

sucName :: Name
sucName :: Name
sucName = Namespace -> String -> Name
Name Namespace
naturalNamespace String
"suc"

zeroName :: Name
zeroName :: Name
zeroName = Namespace -> String -> Name
Name Namespace
naturalNamespace String
"zero"

-- Real numbers

addRealName :: Name
addRealName :: Name
addRealName = Namespace -> String -> Name
Name Namespace
realNamespace String
"+"

divRealName :: Name
divRealName :: Name
divRealName = Namespace -> String -> Name
Name Namespace
realNamespace String
"/"

fromNaturalRealName :: Name
fromNaturalRealName :: Name
fromNaturalRealName = Namespace -> String -> Name
Name Namespace
realNamespace String
"fromNatural"

geRealName :: Name
geRealName :: Name
geRealName = Namespace -> String -> Name
Name Namespace
realNamespace String
">="

gtRealName :: Name
gtRealName :: Name
gtRealName = Namespace -> String -> Name
Name Namespace
realNamespace String
">"

leRealName :: Name
leRealName :: Name
leRealName = Namespace -> String -> Name
Name Namespace
realNamespace String
"<="

ltRealName :: Name
ltRealName :: Name
ltRealName = Namespace -> String -> Name
Name Namespace
realNamespace String
"<"

multRealName :: Name
multRealName :: Name
multRealName = Namespace -> String -> Name
Name Namespace
realNamespace String
"*"

powerRealName :: Name
powerRealName :: Name
powerRealName = Namespace -> String -> Name
Name Namespace
realNamespace String
"^"

subRealName :: Name
subRealName :: Name
subRealName = Namespace -> String -> Name
Name Namespace
realNamespace String
"-"

-- Sets

crossName :: Name
crossName :: Name
crossName = Namespace -> String -> Name
Name Namespace
setNamespace String
"cross"

deleteName :: Name
deleteName :: Name
deleteName = Namespace -> String -> Name
Name Namespace
setNamespace String
"delete"

differenceName :: Name
differenceName :: Name
differenceName = Namespace -> String -> Name
Name Namespace
setNamespace String
"difference"

fromPredicateName :: Name
fromPredicateName :: Name
fromPredicateName = Namespace -> String -> Name
Name Namespace
setNamespace String
"fromPredicate"

insertName :: Name
insertName :: Name
insertName = Namespace -> String -> Name
Name Namespace
setNamespace String
"insert"

intersectName :: Name
intersectName :: Name
intersectName = Namespace -> String -> Name
Name Namespace
setNamespace String
"intersect"

memberName :: Name
memberName :: Name
memberName = Namespace -> String -> Name
Name Namespace
setNamespace String
"member"

properSubsetName :: Name
properSubsetName :: Name
properSubsetName = Namespace -> String -> Name
Name Namespace
setNamespace String
"properSubset"

subsetName :: Name
subsetName :: Name
subsetName = Namespace -> String -> Name
Name Namespace
setNamespace String
"subset"

unionName :: Name
unionName :: Name
unionName = Namespace -> String -> Name
Name Namespace
setNamespace String
"union"