{- |
Module      :  ./Logic/PrintLogics.hs
Description :  Print list of all logics
Copyright   :  (c) Till Mossakowski, and OvGU Magdeburg 2017
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  till@iks.cs.ovgu.de
Stability   :  provisional
Portability :  non-portable (various -fglasgow-exts extensions)

Print list of all logics with some useful information.

-}

module Logic.PrintLogics where

import Comorphisms.LogicList
import Logic.Prover
import Logic.Logic
import Control.Monad
import Data.List

printLogics :: IO ()
printLogics :: IO ()
printLogics = do
  String -> IO ()
putStrLn "*** List of logics in Hets ***"
  (Stability -> IO ()) -> [Stability] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Stability -> IO ()
printLogicsWithStability [Stability
Stable, Stability
Testing, Stability
Experimental, Stability
Unstable]

hasStability :: Stability -> AnyLogic -> Bool
hasStability :: Stability -> AnyLogic -> Bool
hasStability s :: Stability
s (Logic l :: lid
l) = lid -> Stability
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> Stability
stability lid
l Stability -> Stability -> Bool
forall a. Eq a => a -> a -> Bool
== Stability
s

printLogicsWithStability :: Stability -> IO ()
printLogicsWithStability :: Stability -> IO ()
printLogicsWithStability s :: Stability
s = do
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Stability: "String -> String -> String
forall a. [a] -> [a] -> [a]
++Stability -> String
forall a. Show a => a -> String
show Stability
s
  (AnyLogic -> IO ()) -> [AnyLogic] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ AnyLogic -> IO ()
printLogic ([AnyLogic] -> IO ()) -> [AnyLogic] -> IO ()
forall a b. (a -> b) -> a -> b
$ (AnyLogic -> Bool) -> [AnyLogic] -> [AnyLogic]
forall a. (a -> Bool) -> [a] -> [a]
filter (Stability -> AnyLogic -> Bool
hasStability Stability
s) [AnyLogic]
logicList
  
printLogic :: AnyLogic -> IO ()
printLogic :: AnyLogic -> IO ()
printLogic (Logic l :: lid
l) = do
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "  "String -> String -> String
forall a. [a] -> [a] -> [a]
++lid -> String
forall a. Show a => a -> String
show lid
lString -> String -> String
forall a. [a] -> [a] -> [a]
++": "String -> String -> String
forall a. [a] -> [a] -> [a]
++lid -> String
forall lid. Language lid => lid -> String
short_description lid
l
  let ps :: [Prover sign sentence morphism sublogics proof_tree]
ps = lid -> [Prover sign sentence morphism sublogics proof_tree]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [Prover sign sentence morphism sublogics proof_tree]
provers lid
l
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Prover sign sentence morphism sublogics proof_tree] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Prover sign sentence morphism sublogics proof_tree]
ps) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    String -> IO ()
putStr "    provers: "
    String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Prover sign sentence morphism sublogics proof_tree -> String)
-> [Prover sign sentence morphism sublogics proof_tree] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Prover sign sentence morphism sublogics proof_tree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName [Prover sign sentence morphism sublogics proof_tree]
ps