module HOL.Theory
where
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
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
{typeOpMap :: Map Name (Set TypeOp),
constMap :: Map Name (Set Const),
thmMap :: Map Sequent Thm}
deriving (Eq,Ord,Show)
empty :: Theory
empty = Theory {typeOpMap = Map.empty, constMap = Map.empty, thmMap = Map.empty}
fromThmSet :: Set Thm -> Theory
fromThmSet ths =
Theory {typeOpMap = t, constMap = c, thmMap = th}
where
mkSingle k v x = Map.singleton (k x) (v x)
mkGen k v u = Map.unionsWith u . map (mkSingle k v) . Set.toList
mkSet k = mkGen k Set.singleton Set.union
mkSimple k = mkGen k id const
t = mkSet TypeOp.name $ TypeOp.ops ths
c = mkSet Const.name $ Const.consts ths
th = mkSimple Thm.dest ths
union :: Theory -> Theory -> Theory
union thy1 thy2 =
Theory {typeOpMap = t, constMap = c, thmMap = th}
where
Theory {typeOpMap = t1, constMap = c1, thmMap = th1} = thy1
Theory {typeOpMap = t2, constMap = c2, thmMap = th2} = thy2
t = Map.unionWith Set.union t1 t2
c = Map.unionWith Set.union c1 c2
th = Map.union th1 th2
unionList :: [Theory] -> Theory
unionList = foldr union empty
instance TypeOp.HasOps Theory where
ops = TypeOp.ops . Map.elems . typeOpMap
lookupTypeOp :: Theory -> Name -> Maybe TypeOp
lookupTypeOp thy n =
case Map.lookup n $ typeOpMap thy of
Nothing -> Just $ TypeOp.mkUndef n
Just s -> if Set.size s == 1 then Just (Set.findMin s) else Nothing
instance Const.HasConsts Theory where
consts = Const.consts . Map.elems . constMap
lookupConst :: Theory -> Name -> Maybe Const
lookupConst thy n =
case Map.lookup n $ constMap thy of
Nothing -> Just $ Const.mkUndef n
Just s -> if Set.size s == 1 then Just (Set.findMin s) else Nothing
sequents :: Theory -> Set Sequent
sequents = Map.keysSet . thmMap
thms :: Theory -> Set Thm
thms = Set.fromList . Map.elems . thmMap
lookupThm :: Theory -> Sequent -> Maybe Thm
lookupThm thy sq = Map.lookup sq $ thmMap thy
instance Printable Theory where
toDoc thy =
pr "type operator" PP.fsep ts $+$
pr "constant" PP.fsep cs $+$
pr "theorem" PP.vcat ths
where
pr k j xs =
if n == 0 then PP.text "no" <+> ks
else PP.hang (PP.integer n <+> ks <> PP.text ":") 2 xd
where
xd = j (map toDoc (Set.toList xs))
n = toInteger (Set.size xs)
ks = PP.text k <> (if n == 1 then PP.empty else PP.text "s")
ts = TypeOp.ops thy
cs = Const.consts thy
ths = thms thy
standard :: Theory
standard = fromThmSet Thm.standardAxioms