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

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

module HOL.Theory
where

import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Prelude hiding ((<>))
import Text.PrettyPrint ((<>),(<+>),($+$))
import qualified Text.PrettyPrint as PP

import qualified HOL.Const as Const
import HOL.Data
import HOL.Name
import HOL.Print
import HOL.Sequent (Sequent)
import HOL.Thm (Thm)
import qualified HOL.Thm as Thm
import qualified HOL.TypeOp as TypeOp

-------------------------------------------------------------------------------
-- Theories
-------------------------------------------------------------------------------

data Theory =
    Theory
      {Theory -> Map Name (Set TypeOp)
typeOpMap :: Map Name (Set TypeOp),
       Theory -> Map Name (Set Const)
constMap :: Map Name (Set Const),
       Theory -> Map Sequent Thm
thmMap :: Map Sequent Thm}
  deriving (Theory -> Theory -> Bool
(Theory -> Theory -> Bool)
-> (Theory -> Theory -> Bool) -> Eq Theory
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Theory -> Theory -> Bool
$c/= :: Theory -> Theory -> Bool
== :: Theory -> Theory -> Bool
$c== :: Theory -> Theory -> Bool
Eq,Eq Theory
Eq Theory
-> (Theory -> Theory -> Ordering)
-> (Theory -> Theory -> Bool)
-> (Theory -> Theory -> Bool)
-> (Theory -> Theory -> Bool)
-> (Theory -> Theory -> Bool)
-> (Theory -> Theory -> Theory)
-> (Theory -> Theory -> Theory)
-> Ord Theory
Theory -> Theory -> Bool
Theory -> Theory -> Ordering
Theory -> Theory -> Theory
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 :: Theory -> Theory -> Theory
$cmin :: Theory -> Theory -> Theory
max :: Theory -> Theory -> Theory
$cmax :: Theory -> Theory -> Theory
>= :: Theory -> Theory -> Bool
$c>= :: Theory -> Theory -> Bool
> :: Theory -> Theory -> Bool
$c> :: Theory -> Theory -> Bool
<= :: Theory -> Theory -> Bool
$c<= :: Theory -> Theory -> Bool
< :: Theory -> Theory -> Bool
$c< :: Theory -> Theory -> Bool
compare :: Theory -> Theory -> Ordering
$ccompare :: Theory -> Theory -> Ordering
$cp1Ord :: Eq Theory
Ord,Int -> Theory -> ShowS
[Theory] -> ShowS
Theory -> String
(Int -> Theory -> ShowS)
-> (Theory -> String) -> ([Theory] -> ShowS) -> Show Theory
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Theory] -> ShowS
$cshowList :: [Theory] -> ShowS
show :: Theory -> String
$cshow :: Theory -> String
showsPrec :: Int -> Theory -> ShowS
$cshowsPrec :: Int -> Theory -> ShowS
Show)

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

empty :: Theory
empty :: Theory
empty = Theory :: Map Name (Set TypeOp)
-> Map Name (Set Const) -> Map Sequent Thm -> Theory
Theory {typeOpMap :: Map Name (Set TypeOp)
typeOpMap = Map Name (Set TypeOp)
forall k a. Map k a
Map.empty, constMap :: Map Name (Set Const)
constMap = Map Name (Set Const)
forall k a. Map k a
Map.empty, thmMap :: Map Sequent Thm
thmMap = Map Sequent Thm
forall k a. Map k a
Map.empty}

fromThmSet :: Set Thm -> Theory
fromThmSet :: Set Thm -> Theory
fromThmSet Set Thm
ths =
    Theory :: Map Name (Set TypeOp)
-> Map Name (Set Const) -> Map Sequent Thm -> Theory
Theory {typeOpMap :: Map Name (Set TypeOp)
typeOpMap = Map Name (Set TypeOp)
t, constMap :: Map Name (Set Const)
constMap = Map Name (Set Const)
c, thmMap :: Map Sequent Thm
thmMap = Map Sequent Thm
th}
  where
    mkSingle :: (t -> k) -> (t -> a) -> t -> Map k a
mkSingle t -> k
k t -> a
v t
x = k -> a -> Map k a
forall k a. k -> a -> Map k a
Map.singleton (t -> k
k t
x) (t -> a
v t
x)
    mkGen :: (t -> k) -> (t -> a) -> (a -> a -> a) -> Set t -> Map k a
mkGen t -> k
k t -> a
v a -> a -> a
u = (a -> a -> a) -> [Map k a] -> Map k a
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith a -> a -> a
u ([Map k a] -> Map k a) -> (Set t -> [Map k a]) -> Set t -> Map k a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t -> Map k a) -> [t] -> [Map k a]
forall a b. (a -> b) -> [a] -> [b]
map ((t -> k) -> (t -> a) -> t -> Map k a
forall t k a. (t -> k) -> (t -> a) -> t -> Map k a
mkSingle t -> k
k t -> a
v) ([t] -> [Map k a]) -> (Set t -> [t]) -> Set t -> [Map k a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set t -> [t]
forall a. Set a -> [a]
Set.toList
    mkSet :: (a -> k) -> Set a -> Map k (Set a)
mkSet a -> k
k = (a -> k)
-> (a -> Set a)
-> (Set a -> Set a -> Set a)
-> Set a
-> Map k (Set a)
forall k t a.
Ord k =>
(t -> k) -> (t -> a) -> (a -> a -> a) -> Set t -> Map k a
mkGen a -> k
k a -> Set a
forall a. a -> Set a
Set.singleton Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union
    mkSimple :: (b -> k) -> Set b -> Map k b
mkSimple b -> k
k = (b -> k) -> (b -> b) -> (b -> b -> b) -> Set b -> Map k b
forall k t a.
Ord k =>
(t -> k) -> (t -> a) -> (a -> a -> a) -> Set t -> Map k a
mkGen b -> k
k b -> b
forall a. a -> a
id b -> b -> b
forall a b. a -> b -> a
const

    t :: Map Name (Set TypeOp)
t = (TypeOp -> Name) -> Set TypeOp -> Map Name (Set TypeOp)
forall k a. (Ord k, Ord a) => (a -> k) -> Set a -> Map k (Set a)
mkSet TypeOp -> Name
TypeOp.name (Set TypeOp -> Map Name (Set TypeOp))
-> Set TypeOp -> Map Name (Set TypeOp)
forall a b. (a -> b) -> a -> b
$ Set Thm -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
TypeOp.ops Set Thm
ths
    c :: Map Name (Set Const)
c = (Const -> Name) -> Set Const -> Map Name (Set Const)
forall k a. (Ord k, Ord a) => (a -> k) -> Set a -> Map k (Set a)
mkSet Const -> Name
Const.name (Set Const -> Map Name (Set Const))
-> Set Const -> Map Name (Set Const)
forall a b. (a -> b) -> a -> b
$ Set Thm -> Set Const
forall a. HasConsts a => a -> Set Const
Const.consts Set Thm
ths
    th :: Map Sequent Thm
th = (Thm -> Sequent) -> Set Thm -> Map Sequent Thm
forall k b. Ord k => (b -> k) -> Set b -> Map k b
mkSimple Thm -> Sequent
Thm.dest Set Thm
ths

-------------------------------------------------------------------------------
-- Union
-------------------------------------------------------------------------------

union :: Theory -> Theory -> Theory
union :: Theory -> Theory -> Theory
union Theory
thy1 Theory
thy2 =
    Theory :: Map Name (Set TypeOp)
-> Map Name (Set Const) -> Map Sequent Thm -> Theory
Theory {typeOpMap :: Map Name (Set TypeOp)
typeOpMap = Map Name (Set TypeOp)
t, constMap :: Map Name (Set Const)
constMap = Map Name (Set Const)
c, thmMap :: Map Sequent Thm
thmMap = Map Sequent Thm
th}
  where
    Theory {typeOpMap :: Theory -> Map Name (Set TypeOp)
typeOpMap = Map Name (Set TypeOp)
t1, constMap :: Theory -> Map Name (Set Const)
constMap = Map Name (Set Const)
c1, thmMap :: Theory -> Map Sequent Thm
thmMap = Map Sequent Thm
th1} = Theory
thy1
    Theory {typeOpMap :: Theory -> Map Name (Set TypeOp)
typeOpMap = Map Name (Set TypeOp)
t2, constMap :: Theory -> Map Name (Set Const)
constMap = Map Name (Set Const)
c2, thmMap :: Theory -> Map Sequent Thm
thmMap = Map Sequent Thm
th2} = Theory
thy2

    t :: Map Name (Set TypeOp)
t = (Set TypeOp -> Set TypeOp -> Set TypeOp)
-> Map Name (Set TypeOp)
-> Map Name (Set TypeOp)
-> Map Name (Set TypeOp)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set TypeOp -> Set TypeOp -> Set TypeOp
forall a. Ord a => Set a -> Set a -> Set a
Set.union Map Name (Set TypeOp)
t1 Map Name (Set TypeOp)
t2
    c :: Map Name (Set Const)
c = (Set Const -> Set Const -> Set Const)
-> Map Name (Set Const)
-> Map Name (Set Const)
-> Map Name (Set Const)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set Const -> Set Const -> Set Const
forall a. Ord a => Set a -> Set a -> Set a
Set.union Map Name (Set Const)
c1 Map Name (Set Const)
c2
    th :: Map Sequent Thm
th = Map Sequent Thm -> Map Sequent Thm -> Map Sequent Thm
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Sequent Thm
th1 Map Sequent Thm
th2

unionList :: [Theory] -> Theory
unionList :: [Theory] -> Theory
unionList = (Theory -> Theory -> Theory) -> Theory -> [Theory] -> Theory
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Theory -> Theory -> Theory
union Theory
empty

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

instance TypeOp.HasOps Theory where
  ops :: Theory -> Set TypeOp
ops = [Set TypeOp] -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
TypeOp.ops ([Set TypeOp] -> Set TypeOp)
-> (Theory -> [Set TypeOp]) -> Theory -> Set TypeOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name (Set TypeOp) -> [Set TypeOp]
forall k a. Map k a -> [a]
Map.elems (Map Name (Set TypeOp) -> [Set TypeOp])
-> (Theory -> Map Name (Set TypeOp)) -> Theory -> [Set TypeOp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Theory -> Map Name (Set TypeOp)
typeOpMap

lookupTypeOp :: Theory -> Name -> Maybe TypeOp
lookupTypeOp :: Theory -> Name -> Maybe TypeOp
lookupTypeOp Theory
thy Name
n =
    case Name -> Map Name (Set TypeOp) -> Maybe (Set TypeOp)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n (Map Name (Set TypeOp) -> Maybe (Set TypeOp))
-> Map Name (Set TypeOp) -> Maybe (Set TypeOp)
forall a b. (a -> b) -> a -> b
$ Theory -> Map Name (Set TypeOp)
typeOpMap Theory
thy of
      Maybe (Set TypeOp)
Nothing -> TypeOp -> Maybe TypeOp
forall a. a -> Maybe a
Just (TypeOp -> Maybe TypeOp) -> TypeOp -> Maybe TypeOp
forall a b. (a -> b) -> a -> b
$ Name -> TypeOp
TypeOp.mkUndef Name
n
      Just Set TypeOp
s -> if Set TypeOp -> Int
forall a. Set a -> Int
Set.size Set TypeOp
s Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then TypeOp -> Maybe TypeOp
forall a. a -> Maybe a
Just (Set TypeOp -> TypeOp
forall a. Set a -> a
Set.findMin Set TypeOp
s) else Maybe TypeOp
forall a. Maybe a
Nothing

lookupTypeOpUnsafe :: Theory -> Name -> TypeOp
lookupTypeOpUnsafe :: Theory -> Name -> TypeOp
lookupTypeOpUnsafe Theory
thy Name
n =
    case Theory -> Name -> Maybe TypeOp
lookupTypeOp Theory
thy Name
n of
      Just TypeOp
t -> TypeOp
t
      Maybe TypeOp
Nothing -> String -> TypeOp
forall a. HasCallStack => String -> a
error (String -> TypeOp) -> String -> TypeOp
forall a b. (a -> b) -> a -> b
$ String
"ambiguous type operator name " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n

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

instance Const.HasConsts Theory where
  consts :: Theory -> Set Const
consts = [Set Const] -> Set Const
forall a. HasConsts a => a -> Set Const
Const.consts ([Set Const] -> Set Const)
-> (Theory -> [Set Const]) -> Theory -> Set Const
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name (Set Const) -> [Set Const]
forall k a. Map k a -> [a]
Map.elems (Map Name (Set Const) -> [Set Const])
-> (Theory -> Map Name (Set Const)) -> Theory -> [Set Const]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Theory -> Map Name (Set Const)
constMap

lookupConst :: Theory -> Name -> Maybe Const
lookupConst :: Theory -> Name -> Maybe Const
lookupConst Theory
thy Name
n =
    case Name -> Map Name (Set Const) -> Maybe (Set Const)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n (Map Name (Set Const) -> Maybe (Set Const))
-> Map Name (Set Const) -> Maybe (Set Const)
forall a b. (a -> b) -> a -> b
$ Theory -> Map Name (Set Const)
constMap Theory
thy of
      Maybe (Set Const)
Nothing -> Const -> Maybe Const
forall a. a -> Maybe a
Just (Const -> Maybe Const) -> Const -> Maybe Const
forall a b. (a -> b) -> a -> b
$ Name -> Const
Const.mkUndef Name
n
      Just Set Const
s -> if Set Const -> Int
forall a. Set a -> Int
Set.size Set Const
s Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then Const -> Maybe Const
forall a. a -> Maybe a
Just (Set Const -> Const
forall a. Set a -> a
Set.findMin Set Const
s) else Maybe Const
forall a. Maybe a
Nothing

lookupConstUnsafe :: Theory -> Name -> Const
lookupConstUnsafe :: Theory -> Name -> Const
lookupConstUnsafe Theory
thy Name
n =
    case Theory -> Name -> Maybe Const
lookupConst Theory
thy Name
n of
      Just Const
c -> Const
c
      Maybe Const
Nothing -> String -> Const
forall a. HasCallStack => String -> a
error (String -> Const) -> String -> Const
forall a b. (a -> b) -> a -> b
$ String
"ambiguous constant name " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n

-------------------------------------------------------------------------------
-- Theorems
-------------------------------------------------------------------------------

sequents :: Theory -> Set Sequent
sequents :: Theory -> Set Sequent
sequents = Map Sequent Thm -> Set Sequent
forall k a. Map k a -> Set k
Map.keysSet (Map Sequent Thm -> Set Sequent)
-> (Theory -> Map Sequent Thm) -> Theory -> Set Sequent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Theory -> Map Sequent Thm
thmMap

thms :: Theory -> Set Thm
thms :: Theory -> Set Thm
thms = [Thm] -> Set Thm
forall a. Ord a => [a] -> Set a
Set.fromList ([Thm] -> Set Thm) -> (Theory -> [Thm]) -> Theory -> Set Thm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Sequent Thm -> [Thm]
forall k a. Map k a -> [a]
Map.elems (Map Sequent Thm -> [Thm])
-> (Theory -> Map Sequent Thm) -> Theory -> [Thm]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Theory -> Map Sequent Thm
thmMap

lookupThm :: Theory -> Sequent -> Maybe Thm
lookupThm :: Theory -> Sequent -> Maybe Thm
lookupThm Theory
thy Sequent
sq = Sequent -> Map Sequent Thm -> Maybe Thm
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Sequent
sq (Map Sequent Thm -> Maybe Thm) -> Map Sequent Thm -> Maybe Thm
forall a b. (a -> b) -> a -> b
$ Theory -> Map Sequent Thm
thmMap Theory
thy

-------------------------------------------------------------------------------
-- Printing
-------------------------------------------------------------------------------

instance Printable Theory where
  toDoc :: Theory -> Doc
toDoc Theory
thy =
      String -> ([Doc] -> Doc) -> Set TypeOp -> Doc
forall a. Printable a => String -> ([Doc] -> Doc) -> Set a -> Doc
pr String
"type operator" [Doc] -> Doc
PP.fsep Set TypeOp
ts Doc -> Doc -> Doc
$+$
      String -> ([Doc] -> Doc) -> Set Const -> Doc
forall a. Printable a => String -> ([Doc] -> Doc) -> Set a -> Doc
pr String
"constant" [Doc] -> Doc
PP.fsep Set Const
cs Doc -> Doc -> Doc
$+$
      String -> ([Doc] -> Doc) -> Set Thm -> Doc
forall a. Printable a => String -> ([Doc] -> Doc) -> Set a -> Doc
pr String
"theorem" [Doc] -> Doc
PP.vcat Set Thm
ths
    where
      pr :: String -> ([Doc] -> Doc) -> Set a -> Doc
pr String
k [Doc] -> Doc
j Set a
xs =
          if Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then String -> Doc
PP.text String
"no" Doc -> Doc -> Doc
<+> Doc
ks
          else Doc -> Int -> Doc -> Doc
PP.hang (Integer -> Doc
PP.integer Integer
n Doc -> Doc -> Doc
<+> Doc
ks Doc -> Doc -> Doc
<> String -> Doc
PP.text String
":") Int
2 Doc
xd
        where
          xd :: Doc
xd = [Doc] -> Doc
j ((a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Printable a => a -> Doc
toDoc (Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
xs))
          n :: Integer
n = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Set a -> Int
forall a. Set a -> Int
Set.size Set a
xs)
          ks :: Doc
ks = String -> Doc
PP.text String
k Doc -> Doc -> Doc
<> (if Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 then Doc
PP.empty else String -> Doc
PP.text String
"s")

      ts :: Set TypeOp
ts = Theory -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
TypeOp.ops Theory
thy
      cs :: Set Const
cs = Theory -> Set Const
forall a. HasConsts a => a -> Set Const
Const.consts Theory
thy
      ths :: Set Thm
ths = Theory -> Set Thm
thms Theory
thy

-------------------------------------------------------------------------------
-- A minimal theory containing the standard axioms
-------------------------------------------------------------------------------

standard :: Theory
standard :: Theory
standard = Set Thm -> Theory
fromThmSet Set Thm
Thm.standardAxioms