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

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

module HOL.Sequent
where

import qualified Data.Foldable as Foldable
import Data.Maybe (isNothing,fromMaybe)
import Data.Set (Set)
import qualified Data.Set as Set
import qualified HOL.Const as Const
import qualified HOL.Subst as Subst
import HOL.TermAlpha (TermAlpha)
import qualified HOL.TermAlpha as TermAlpha
import qualified HOL.TypeOp as TypeOp
import qualified HOL.TypeVar as TypeVar
import HOL.Util (mkUnsafe1,mkUnsafe2)
import qualified HOL.Var as Var

-------------------------------------------------------------------------------
-- Sequents
-------------------------------------------------------------------------------

data Sequent =
    Sequent
      {Sequent -> TermAlpha
concl :: TermAlpha,
       Sequent -> Set TermAlpha
hyp :: Set TermAlpha}
  deriving (Sequent -> Sequent -> Bool
(Sequent -> Sequent -> Bool)
-> (Sequent -> Sequent -> Bool) -> Eq Sequent
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sequent -> Sequent -> Bool
$c/= :: Sequent -> Sequent -> Bool
== :: Sequent -> Sequent -> Bool
$c== :: Sequent -> Sequent -> Bool
Eq,Eq Sequent
Eq Sequent
-> (Sequent -> Sequent -> Ordering)
-> (Sequent -> Sequent -> Bool)
-> (Sequent -> Sequent -> Bool)
-> (Sequent -> Sequent -> Bool)
-> (Sequent -> Sequent -> Bool)
-> (Sequent -> Sequent -> Sequent)
-> (Sequent -> Sequent -> Sequent)
-> Ord Sequent
Sequent -> Sequent -> Bool
Sequent -> Sequent -> Ordering
Sequent -> Sequent -> Sequent
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Sequent -> Sequent -> Sequent
$cmin :: Sequent -> Sequent -> Sequent
max :: Sequent -> Sequent -> Sequent
$cmax :: Sequent -> Sequent -> Sequent
>= :: Sequent -> Sequent -> Bool
$c>= :: Sequent -> Sequent -> Bool
> :: Sequent -> Sequent -> Bool
$c> :: Sequent -> Sequent -> Bool
<= :: Sequent -> Sequent -> Bool
$c<= :: Sequent -> Sequent -> Bool
< :: Sequent -> Sequent -> Bool
$c< :: Sequent -> Sequent -> Bool
compare :: Sequent -> Sequent -> Ordering
$ccompare :: Sequent -> Sequent -> Ordering
$cp1Ord :: Eq Sequent
Ord,Int -> Sequent -> ShowS
[Sequent] -> ShowS
Sequent -> String
(Int -> Sequent -> ShowS)
-> (Sequent -> String) -> ([Sequent] -> ShowS) -> Show Sequent
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sequent] -> ShowS
$cshowList :: [Sequent] -> ShowS
show :: Sequent -> String
$cshow :: Sequent -> String
showsPrec :: Int -> Sequent -> ShowS
$cshowsPrec :: Int -> Sequent -> ShowS
Show)

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

mk :: Set TermAlpha -> TermAlpha -> Maybe Sequent
mk :: Set TermAlpha -> TermAlpha -> Maybe Sequent
mk Set TermAlpha
h TermAlpha
c =
    if Bool
b then Sequent -> Maybe Sequent
forall a. a -> Maybe a
Just Sequent
sq else Maybe Sequent
forall a. Maybe a
Nothing
  where
    b :: Bool
b = (TermAlpha -> Bool) -> Set TermAlpha -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
Foldable.all TermAlpha -> Bool
TermAlpha.isBool Set TermAlpha
h Bool -> Bool -> Bool
&& TermAlpha -> Bool
TermAlpha.isBool TermAlpha
c
    sq :: Sequent
sq = Sequent :: TermAlpha -> Set TermAlpha -> Sequent
Sequent {hyp :: Set TermAlpha
hyp = Set TermAlpha
h, concl :: TermAlpha
concl = TermAlpha
c}

mkUnsafe :: Set TermAlpha -> TermAlpha -> Sequent
mkUnsafe :: Set TermAlpha -> TermAlpha -> Sequent
mkUnsafe = String
-> (Set TermAlpha -> TermAlpha -> Maybe Sequent)
-> Set TermAlpha
-> TermAlpha
-> Sequent
forall a b c. String -> (a -> b -> Maybe c) -> a -> b -> c
mkUnsafe2 String
"HOL.Sequent.mk" Set TermAlpha -> TermAlpha -> Maybe Sequent
mk

dest :: Sequent -> (Set TermAlpha, TermAlpha)
dest :: Sequent -> (Set TermAlpha, TermAlpha)
dest (Sequent {hyp :: Sequent -> Set TermAlpha
hyp = Set TermAlpha
h, concl :: Sequent -> TermAlpha
concl = TermAlpha
c}) = (Set TermAlpha
h,TermAlpha
c)

nullHyp :: Sequent -> Bool
nullHyp :: Sequent -> Bool
nullHyp = Set TermAlpha -> Bool
forall a. Set a -> Bool
Set.null (Set TermAlpha -> Bool)
-> (Sequent -> Set TermAlpha) -> Sequent -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sequent -> Set TermAlpha
hyp

mkNullHyp :: TermAlpha -> Maybe Sequent
mkNullHyp :: TermAlpha -> Maybe Sequent
mkNullHyp = Set TermAlpha -> TermAlpha -> Maybe Sequent
mk Set TermAlpha
forall a. Set a
Set.empty

mkNullHypUnsafe :: TermAlpha -> Sequent
mkNullHypUnsafe :: TermAlpha -> Sequent
mkNullHypUnsafe = String -> (TermAlpha -> Maybe Sequent) -> TermAlpha -> Sequent
forall a b. String -> (a -> Maybe b) -> a -> b
mkUnsafe1 String
"HOL.Sequent.mkNullHyp" TermAlpha -> Maybe Sequent
mkNullHyp

-------------------------------------------------------------------------------
-- Type variables
-------------------------------------------------------------------------------

instance TypeVar.HasVars Sequent where
  vars :: Sequent -> Set TypeVar
vars (Sequent {hyp :: Sequent -> Set TermAlpha
hyp = Set TermAlpha
h, concl :: Sequent -> TermAlpha
concl = TermAlpha
c}) =
      Set TypeVar -> Set TypeVar -> Set TypeVar
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set TermAlpha -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
TypeVar.vars Set TermAlpha
h) (TermAlpha -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
TypeVar.vars TermAlpha
c)

-------------------------------------------------------------------------------
-- Type operators
-------------------------------------------------------------------------------

instance TypeOp.HasOps Sequent where
  ops :: Sequent -> Set TypeOp
ops (Sequent {hyp :: Sequent -> Set TermAlpha
hyp = Set TermAlpha
h, concl :: Sequent -> TermAlpha
concl = TermAlpha
c}) =
      Set TypeOp -> Set TypeOp -> Set TypeOp
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set TermAlpha -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
TypeOp.ops Set TermAlpha
h) (TermAlpha -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
TypeOp.ops TermAlpha
c)

-------------------------------------------------------------------------------
-- Constants
-------------------------------------------------------------------------------

instance Const.HasConsts Sequent where
  consts :: Sequent -> Set Const
consts (Sequent {hyp :: Sequent -> Set TermAlpha
hyp = Set TermAlpha
h, concl :: Sequent -> TermAlpha
concl = TermAlpha
c}) =
      Set Const -> Set Const -> Set Const
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set TermAlpha -> Set Const
forall a. HasConsts a => a -> Set Const
Const.consts Set TermAlpha
h) (TermAlpha -> Set Const
forall a. HasConsts a => a -> Set Const
Const.consts TermAlpha
c)

-------------------------------------------------------------------------------
-- Free variables
-------------------------------------------------------------------------------

instance Var.HasFree Sequent where
  free :: Sequent -> Set Var
free (Sequent {hyp :: Sequent -> Set TermAlpha
hyp = Set TermAlpha
h, concl :: Sequent -> TermAlpha
concl = TermAlpha
c}) =
      Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set TermAlpha -> Set Var
forall a. HasFree a => a -> Set Var
Var.free Set TermAlpha
h) (TermAlpha -> Set Var
forall a. HasFree a => a -> Set Var
Var.free TermAlpha
c)

-------------------------------------------------------------------------------
-- Substitutions
-------------------------------------------------------------------------------

instance Subst.CanSubst Sequent where
  basicSubst :: Sequent -> Subst -> (Maybe Sequent, Subst)
basicSubst (Sequent {hyp :: Sequent -> Set TermAlpha
hyp = Set TermAlpha
h, concl :: Sequent -> TermAlpha
concl = TermAlpha
c}) Subst
sub =
      (Maybe Sequent
seq',Subst
sub'')
    where
      (Maybe (Set TermAlpha)
h',Subst
sub') = Set TermAlpha -> Subst -> (Maybe (Set TermAlpha), Subst)
forall a. CanSubst a => a -> Subst -> (Maybe a, Subst)
Subst.basicSubst Set TermAlpha
h Subst
sub
      (Maybe TermAlpha
c',Subst
sub'') = TermAlpha -> Subst -> (Maybe TermAlpha, Subst)
forall a. CanSubst a => a -> Subst -> (Maybe a, Subst)
Subst.basicSubst TermAlpha
c Subst
sub'
      seq' :: Maybe Sequent
seq' = if Maybe (Set TermAlpha) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (Set TermAlpha)
h' Bool -> Bool -> Bool
&& Maybe TermAlpha -> Bool
forall a. Maybe a -> Bool
isNothing Maybe TermAlpha
c' then Maybe Sequent
forall a. Maybe a
Nothing
             else Sequent -> Maybe Sequent
forall a. a -> Maybe a
Just (Sequent -> Maybe Sequent) -> Sequent -> Maybe Sequent
forall a b. (a -> b) -> a -> b
$ Sequent :: TermAlpha -> Set TermAlpha -> Sequent
Sequent {hyp :: Set TermAlpha
hyp = Set TermAlpha -> Maybe (Set TermAlpha) -> Set TermAlpha
forall a. a -> Maybe a -> a
fromMaybe Set TermAlpha
h Maybe (Set TermAlpha)
h', concl :: TermAlpha
concl = TermAlpha -> Maybe TermAlpha -> TermAlpha
forall a. a -> Maybe a -> a
fromMaybe TermAlpha
c Maybe TermAlpha
c'}

-------------------------------------------------------------------------------
-- Standard axioms
-------------------------------------------------------------------------------

axiomOfExtensionality :: Sequent
axiomOfExtensionality :: Sequent
axiomOfExtensionality = TermAlpha -> Sequent
mkNullHypUnsafe TermAlpha
TermAlpha.axiomOfExtensionality

axiomOfChoice :: Sequent
axiomOfChoice :: Sequent
axiomOfChoice = TermAlpha -> Sequent
mkNullHypUnsafe TermAlpha
TermAlpha.axiomOfChoice

axiomOfInfinity :: Sequent
axiomOfInfinity :: Sequent
axiomOfInfinity = TermAlpha -> Sequent
mkNullHypUnsafe  TermAlpha
TermAlpha.axiomOfInfinity

standardAxioms :: Set Sequent
standardAxioms :: Set Sequent
standardAxioms =
    [Sequent] -> Set Sequent
forall a. Ord a => [a] -> Set a
Set.fromList
      [Sequent
axiomOfExtensionality,
       Sequent
axiomOfChoice,
       Sequent
axiomOfInfinity]