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
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)
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 :: 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
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
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
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
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
standard :: Theory
standard :: Theory
standard = Set Thm -> Theory
fromThmSet Set Thm
Thm.standardAxioms