{-# LANGUAGE CPP, RankNTypes #-}
{- |
Module      :./CMDL/InfoCommands.hs
Description : CMDL interface commands
Copyright   : uni-bremen and DFKI
License     : GPLv2 or higher, see LICENSE.txt
Maintainer  : r.pascanu@jacobs-university.de
Stability   : provisional
Portability : portable

CMDL.InfoCommands contains all commands
that provides information about the state
of the development graph and selected
theories
-}

module CMDL.InfoCommands
       ( cNodes
       , cShowDgGoals
       , cShowNodeProvenGoals
       , cShowNodeUnprovenGoals
       , cRedoHistory
       , cCurrentComorphism
       , cShowTaxonomy
       , cShowTheory
       , cShowTheoryGoals
       , cUndoHistory
       , cEdges
       , cShowNodeAxioms
       , cInfo
       , cComorphismsTo
       , cInfoCurrent
       , cShowConcept
       , cNodeNumber
       , cHelp
       ) where


#ifdef UNI_PACKAGE
import GUI.Taxonomy
#endif

import CMDL.DataTypesUtils
import CMDL.DataTypes
import CMDL.Shell (nodeNames)
import CMDL.Utils

import Static.GTheory
import Static.DevGraph
import Static.PrintDevGraph (showLEdge)

import Common.AS_Annotation (SenAttr (isAxiom))
import Common.DocUtils (showDoc)
import Common.Taxonomy (TaxoGraphKind (..))
import Common.Utils (trim)
import qualified Common.OrderedMap as OMap
import Common.GraphAlgo (yen)

import Proofs.AbstractState (isSubElemG, pathToComorphism)

import Data.Graph.Inductive.Graph (LNode, LEdge, Node)
import Data.List

import Logic.Prover (SenStatus)
import Logic.Comorphism (AnyComorphism)
import Logic.Grothendieck (logicGraph2Graph)

import Comorphisms.LogicGraph (logicGraph)

import Interfaces.Command (cmdNameStr, describeCmd, showCmd)
import Interfaces.DataTypes
import Interfaces.Utils

-- show list of all goals(i.e. prints their name)
cShowDgGoals :: CmdlState -> IO CmdlState
cShowDgGoals :: CmdlState -> IO CmdlState
cShowDgGoals state :: CmdlState
state
 = case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
    -- nothing to print
    Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state
    Just dgState :: IntIState
dgState -> let
         -- list of all nodes
         ls :: [LNode DGNodeLab]
ls = IntIState -> [LNode DGNodeLab]
getAllNodes IntIState
dgState
         -- compute list of node goals
         nodeGoals :: [String]
nodeGoals = [LNode DGNodeLab] -> [String]
forall a. [(a, DGNodeLab)] -> [String]
nodeNames ([LNode DGNodeLab] -> [String]) -> [LNode DGNodeLab] -> [String]
forall a b. (a -> b) -> a -> b
$ (LNode DGNodeLab -> Bool) -> [LNode DGNodeLab] -> [LNode DGNodeLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (DGNodeLab -> Bool
hasOpenGoals (DGNodeLab -> Bool)
-> (LNode DGNodeLab -> DGNodeLab) -> LNode DGNodeLab -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LNode DGNodeLab -> DGNodeLab
forall a b. (a, b) -> b
snd) [LNode DGNodeLab]
ls
         -- list of all goal edge names
         edgeGoals :: [String]
edgeGoals = ((String, LEdge DGLinkLab) -> String)
-> [(String, LEdge DGLinkLab)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, LEdge DGLinkLab) -> String
forall a b. (a, b) -> a
fst ([(String, LEdge DGLinkLab)] -> [String])
-> [(String, LEdge DGLinkLab)] -> [String]
forall a b. (a -> b) -> a -> b
$ ((String, LEdge DGLinkLab) -> Bool)
-> [(String, LEdge DGLinkLab)] -> [(String, LEdge DGLinkLab)]
forall a. (a -> Bool) -> [a] -> [a]
filter (LEdge DGLinkLab -> Bool
edgeContainsGoals (LEdge DGLinkLab -> Bool)
-> ((String, LEdge DGLinkLab) -> LEdge DGLinkLab)
-> (String, LEdge DGLinkLab)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, LEdge DGLinkLab) -> LEdge DGLinkLab
forall a b. (a, b) -> b
snd)
           ([(String, LEdge DGLinkLab)] -> [(String, LEdge DGLinkLab)])
-> [(String, LEdge DGLinkLab)] -> [(String, LEdge DGLinkLab)]
forall a b. (a -> b) -> a -> b
$ [LNode DGNodeLab]
-> [LEdge DGLinkLab] -> [(String, LEdge DGLinkLab)]
createEdgeNames [LNode DGNodeLab]
ls ([LEdge DGLinkLab] -> [(String, LEdge DGLinkLab)])
-> [LEdge DGLinkLab] -> [(String, LEdge DGLinkLab)]
forall a b. (a -> b) -> a -> b
$ IntIState -> [LEdge DGLinkLab]
getAllEdges IntIState
dgState
     -- print sorted version of the list
      in CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlState -> CmdlState
genMessage [] ([String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. Ord a => [a] -> [a]
sort ([String]
nodeGoals [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
edgeGoals)) CmdlState
state


{- local function that computes the theory of a node but it
   keeps only the goal theory -}
getGoalThS :: CmdlUseTranslation -> Int -> CmdlState -> [String]
getGoalThS :: CmdlUseTranslation -> Int -> CmdlState -> [String]
getGoalThS useTrans :: CmdlUseTranslation
useTrans x :: Int
x state :: CmdlState
state
 = case CmdlUseTranslation -> Int -> CmdlState -> Maybe G_theory
getTh CmdlUseTranslation
useTrans Int
x CmdlState
state of
    Nothing -> []
    Just th :: G_theory
th ->
      let nwth :: G_theory
nwth = case G_theory
th of
                  G_theory x1 :: lid
x1 syn :: Maybe IRI
syn x2 :: ExtSign sign symbol
x2 x3 :: SigId
x3 thSens :: ThSens sentence (AnyComorphism, BasicProof)
thSens x4 :: ThId
x4 ->
                    lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
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
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
x1 Maybe IRI
syn ExtSign sign symbol
x2 SigId
x3
                       ((SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter (\ s :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s -> Bool -> Bool
not (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s) Bool -> Bool -> Bool
&&
                                          Bool -> Bool
not (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvenSenStatus SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s))
                       ThSens sentence (AnyComorphism, BasicProof)
thSens) ThId
x4
      in [G_theory -> ShowS
forall a. Pretty a => a -> ShowS
showDoc G_theory
nwth "\n"]

{- local function that computes the theory of a node
   that takes into consideration translated theories in
   the selection too and returns the theory as a string -}
getThS :: CmdlUseTranslation -> Int -> CmdlState -> [String]
getThS :: CmdlUseTranslation -> Int -> CmdlState -> [String]
getThS useTrans :: CmdlUseTranslation
useTrans x :: Int
x state :: CmdlState
state =
  case CmdlUseTranslation -> Int -> CmdlState -> Maybe G_theory
getTh CmdlUseTranslation
useTrans Int
x CmdlState
state of
    Nothing -> ["Could not find a theory"]
    Just th :: G_theory
th -> [G_theory -> ShowS
forall a. Pretty a => a -> ShowS
showDoc G_theory
th "\n"]

getInfoFromNodes :: String -> ([Node] -> [String]) -> CmdlState -> IO CmdlState
getInfoFromNodes :: String -> ([Int] -> [String]) -> CmdlState -> IO CmdlState
getInfoFromNodes input :: String
input f :: [Int] -> [String]
f state :: CmdlState
state =
  case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
    Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state
    Just dgState :: IntIState
dgState -> let (errors :: String
errors, nodes :: [Int]
nodes) = String -> IntIState -> (String, [Int])
getInputNodes String
input IntIState
dgState
                     in CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (if [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
nodes
                                  then String -> Int -> CmdlState -> CmdlState
genMsgAndCode String
errors 1 CmdlState
state
                                  else String -> String -> CmdlState -> CmdlState
genMessage String
errors
                                         (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [Int] -> [String]
f [Int]
nodes) CmdlState
state)

cShowFromNode :: (forall a . SenStatus a (AnyComorphism, BasicProof) -> Bool)
                                     -- ^ what sentences to show
               -> String             -- input string containing node-names
               -> CmdlState          -- the state
               -> IO CmdlState
cShowFromNode :: (forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool)
-> String -> CmdlState -> IO CmdlState
cShowFromNode f :: forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
f input :: String
input state :: CmdlState
state =
  String -> ([Int] -> [String]) -> CmdlState -> IO CmdlState
getInfoFromNodes String
input ((Int -> [String]) -> [Int] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ n :: Int
n ->
                case CmdlUseTranslation -> Int -> CmdlState -> Maybe G_theory
getTh CmdlUseTranslation
Dont_translate Int
n CmdlState
state of
                  Nothing -> []
                  Just th :: G_theory
th -> case G_theory
th of
                                 G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _ -> ThSens sentence (AnyComorphism, BasicProof) -> [String]
forall k a. Ord k => OMap k a -> [k]
OMap.keys (ThSens sentence (AnyComorphism, BasicProof) -> [String])
-> ThSens sentence (AnyComorphism, BasicProof) -> [String]
forall a b. (a -> b) -> a -> b
$
                                   (SenStatus sentence (AnyComorphism, BasicProof) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter SenStatus sentence (AnyComorphism, BasicProof) -> Bool
forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
f ThSens sentence (AnyComorphism, BasicProof)
sens)) CmdlState
state

cShowNodeProvenGoals :: String -> CmdlState -> IO CmdlState
cShowNodeProvenGoals :: String -> CmdlState -> IO CmdlState
cShowNodeProvenGoals =
  (forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool)
-> String -> CmdlState -> IO CmdlState
cShowFromNode (\ s :: SenStatus a (AnyComorphism, BasicProof)
s -> Bool -> Bool
not (SenStatus a (AnyComorphism, BasicProof) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom SenStatus a (AnyComorphism, BasicProof)
s) Bool -> Bool -> Bool
&& SenStatus a (AnyComorphism, BasicProof) -> Bool
forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvenSenStatus SenStatus a (AnyComorphism, BasicProof)
s)

cShowNodeUnprovenGoals :: String -> CmdlState -> IO CmdlState
cShowNodeUnprovenGoals :: String -> CmdlState -> IO CmdlState
cShowNodeUnprovenGoals =
  (forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool)
-> String -> CmdlState -> IO CmdlState
cShowFromNode (\ s :: SenStatus a (AnyComorphism, BasicProof)
s -> Bool -> Bool
not (SenStatus a (AnyComorphism, BasicProof) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom SenStatus a (AnyComorphism, BasicProof)
s) Bool -> Bool -> Bool
&& Bool -> Bool
not (SenStatus a (AnyComorphism, BasicProof) -> Bool
forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvenSenStatus SenStatus a (AnyComorphism, BasicProof)
s))

cShowNodeAxioms :: String -> CmdlState -> IO CmdlState
cShowNodeAxioms :: String -> CmdlState -> IO CmdlState
cShowNodeAxioms = (forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool)
-> String -> CmdlState -> IO CmdlState
cShowFromNode forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom

-- show theory of input nodes
cShowTheory :: CmdlUseTranslation -> String -> CmdlState -> IO CmdlState
cShowTheory :: CmdlUseTranslation -> String -> CmdlState -> IO CmdlState
cShowTheory useTrans :: CmdlUseTranslation
useTrans input :: String
input state :: CmdlState
state =
  String -> ([Int] -> [String]) -> CmdlState -> IO CmdlState
getInfoFromNodes String
input ((Int -> [String]) -> [Int] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ n :: Int
n -> CmdlUseTranslation -> Int -> CmdlState -> [String]
getThS CmdlUseTranslation
useTrans Int
n CmdlState
state)) CmdlState
state

-- show theory of all goals
cShowTheoryGoals :: String -> CmdlState -> IO CmdlState
cShowTheoryGoals :: String -> CmdlState -> IO CmdlState
cShowTheoryGoals input :: String
input st :: CmdlState
st =
  String -> ([Int] -> [String]) -> CmdlState -> IO CmdlState
getInfoFromNodes String
input ((Int -> [String]) -> [Int] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ n :: Int
n -> CmdlUseTranslation -> Int -> CmdlState -> [String]
getGoalThS CmdlUseTranslation
Do_translate Int
n CmdlState
st)) CmdlState
st

showNodeInfo :: LNode DGNodeLab -> String
showNodeInfo :: LNode DGNodeLab -> String
showNodeInfo (i :: Int
i, l :: DGNodeLab
l) =
  (if DGNodeLab -> Bool
isDGRef DGNodeLab
l
     then ("reference " String -> ShowS
forall a. [a] -> [a] -> [a]
++)
     else if DGNodeLab -> Bool
isInternalNode DGNodeLab
l then ("internal " String -> ShowS
forall a. [a] -> [a] -> [a]
++) else ShowS
forall a. a -> a
id)
  "node " String -> ShowS
forall a. [a] -> [a] -> [a]
++ DGNodeLab -> String
getDGNodeName DGNodeLab
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ DGNodeLab -> ShowS
forall a. Pretty a => a -> ShowS
showDoc DGNodeLab
l ""

showEdgeInfo :: LEdge DGLinkLab -> String
showEdgeInfo :: LEdge DGLinkLab -> String
showEdgeInfo e :: LEdge DGLinkLab
e@(_, _, l :: DGLinkLab
l) = LEdge DGLinkLab -> String
showLEdge LEdge DGLinkLab
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ DGLinkLab -> ShowS
forall a. Pretty a => a -> ShowS
showDoc DGLinkLab
l ""

-- show all information of selection
cInfoCurrent :: CmdlState -> IO CmdlState
cInfoCurrent :: CmdlState -> IO CmdlState
cInfoCurrent state :: CmdlState
state =
  case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
    -- nothing selected
    Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state
    Just ps :: IntIState
ps -> let (errors :: String
errors, nodes :: [LNode DGNodeLab]
nodes) = IntIState -> (String, [LNode DGNodeLab])
getSelectedDGNodes IntIState
ps
                in if [LNode DGNodeLab] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LNode DGNodeLab]
nodes
                     then CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode String
errors 1 CmdlState
state
                     else String -> CmdlState -> IO CmdlState
cInfo ([String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [LNode DGNodeLab] -> [String]
forall a. [(a, DGNodeLab)] -> [String]
nodeNames [LNode DGNodeLab]
nodes) CmdlState
state

cComorphismsTo :: String -> CmdlState -> IO CmdlState
cComorphismsTo :: String -> CmdlState -> IO CmdlState
cComorphismsTo input :: String
input state :: CmdlState
state =
  case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
    -- nothing selected
    Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state
    Just ps :: IntIState
ps -> case IntIState -> Maybe G_sublogics
getCurrentSublogic IntIState
ps of
                Just start :: G_sublogics
start -> case String -> Maybe G_sublogics
parseSublogics String
input of
                                Just end :: G_sublogics
end ->
                                 let cmors :: [([((G_sublogics, Maybe AnyComorphism), AnyComorphism)],
  (G_sublogics, Maybe AnyComorphism))]
cmors = Int
-> (G_sublogics, Maybe AnyComorphism)
-> ((G_sublogics, Maybe AnyComorphism) -> Bool)
-> Graph (G_sublogics, Maybe AnyComorphism) AnyComorphism
-> [([((G_sublogics, Maybe AnyComorphism), AnyComorphism)],
     (G_sublogics, Maybe AnyComorphism))]
forall node edge.
(Ord node, Eq edge, Show node, Show edge) =>
Int
-> node
-> (node -> Bool)
-> Graph node edge
-> [([(node, edge)], node)]
yen 10 (G_sublogics
start, Maybe AnyComorphism
forall a. Maybe a
Nothing)
                                          (\ (l :: G_sublogics
l, _) -> G_sublogics -> G_sublogics -> Bool
isSubElemG G_sublogics
l G_sublogics
end)
                                          (LogicGraph
-> Graph (G_sublogics, Maybe AnyComorphism) AnyComorphism
logicGraph2Graph LogicGraph
logicGraph)
                                     cmor :: [String]
cmor = (([((G_sublogics, Maybe AnyComorphism), AnyComorphism)],
  (G_sublogics, Maybe AnyComorphism))
 -> String)
-> [([((G_sublogics, Maybe AnyComorphism), AnyComorphism)],
     (G_sublogics, Maybe AnyComorphism))]
-> [String]
forall a b. (a -> b) -> [a] -> [b]
map (AnyComorphism -> String
forall a. Show a => a -> String
show (AnyComorphism -> String)
-> (([((G_sublogics, Maybe AnyComorphism), AnyComorphism)],
     (G_sublogics, Maybe AnyComorphism))
    -> AnyComorphism)
-> ([((G_sublogics, Maybe AnyComorphism), AnyComorphism)],
    (G_sublogics, Maybe AnyComorphism))
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([((G_sublogics, Maybe AnyComorphism), AnyComorphism)],
 (G_sublogics, Maybe AnyComorphism))
-> AnyComorphism
forall t1 t.
([((G_sublogics, t1), AnyComorphism)], (G_sublogics, t))
-> AnyComorphism
pathToComorphism) [([((G_sublogics, Maybe AnyComorphism), AnyComorphism)],
  (G_sublogics, Maybe AnyComorphism))]
cmors
                                 in CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlState -> CmdlState
genMessage ""
                                              ([String] -> String
unlines [String]
cmor) CmdlState
state
                                Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode
                                            ("Invalid logic " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
input) 1 CmdlState
state
                Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode
                                     "No node(s) selected!" 1 CmdlState
state

-- show all information of input
cInfo :: String -> CmdlState -> IO CmdlState
cInfo :: String -> CmdlState -> IO CmdlState
cInfo input :: String
input state :: CmdlState
state =
  case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
    -- error message
    Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode "No library loaded" 1 CmdlState
state
    Just dgS :: IntIState
dgS ->
     let (nds :: [String]
nds, edg :: [String]
edg, nbEdg :: [String]
nbEdg, errs :: [String]
errs) = String -> ([String], [String], [String], [String])
decomposeIntoGoals String
input
         tmpErrs :: String
tmpErrs = [String] -> String
prettyPrintErrList [String]
errs
     in case ([String]
nds, [String]
edg, [String]
nbEdg) of
          ([], [], []) -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode ("Nothing from the input "
                                       String -> ShowS
forall a. [a] -> [a] -> [a]
++ "could be processed") 1 CmdlState
state
          (_, _, _) ->
            let lsNodes :: [LNode DGNodeLab]
lsNodes = IntIState -> [LNode DGNodeLab]
getAllNodes IntIState
dgS
                lsEdges :: [LEdge DGLinkLab]
lsEdges = IntIState -> [LEdge DGLinkLab]
getAllEdges IntIState
dgS
                (errs'' :: [String]
errs'', listEdges :: [LEdge DGLinkLab]
listEdges) = [String]
-> [String]
-> [LNode DGNodeLab]
-> [LEdge DGLinkLab]
-> ([String], [LEdge DGLinkLab])
obtainEdgeList [String]
edg [String]
nbEdg [LNode DGNodeLab]
lsNodes [LEdge DGLinkLab]
lsEdges
                (errs' :: [String]
errs', listNodes :: [LNode DGNodeLab]
listNodes) = [String] -> [LNode DGNodeLab] -> ([String], [LNode DGNodeLab])
obtainNodeList [String]
nds [LNode DGNodeLab]
lsNodes
                strsNode :: [String]
strsNode = (LNode DGNodeLab -> String) -> [LNode DGNodeLab] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map LNode DGNodeLab -> String
showNodeInfo [LNode DGNodeLab]
listNodes
                strsEdge :: [String]
strsEdge = (LEdge DGLinkLab -> String) -> [LEdge DGLinkLab] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map LEdge DGLinkLab -> String
showEdgeInfo [LEdge DGLinkLab]
listEdges
                tmpErrs' :: String
tmpErrs' = String
tmpErrs String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
prettyPrintErrList [String]
errs'
                tmpErrs'' :: String
tmpErrs'' = String
tmpErrs' String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
prettyPrintErrList [String]
errs''
             in CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlState -> CmdlState
genMessage String
tmpErrs''
                         (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n\n" ([String]
strsNode [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
strsEdge)) CmdlState
state

taxoShowGeneric :: TaxoGraphKind -> CmdlState -> [LNode DGNodeLab] -> IO ()
#ifdef UNI_PACKAGE
taxoShowGeneric :: TaxoGraphKind -> CmdlState -> [LNode DGNodeLab] -> IO ()
taxoShowGeneric kind :: TaxoGraphKind
kind state :: CmdlState
state ls :: [LNode DGNodeLab]
ls =
  case [LNode DGNodeLab]
ls of
    (nb :: Int
nb, nlab :: DGNodeLab
nlab) : ll :: [LNode DGNodeLab]
ll ->
     case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
      Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Just _ ->
       case CmdlUseTranslation -> Int -> CmdlState -> Maybe G_theory
getTh CmdlUseTranslation
Do_translate Int
nb CmdlState
state of
       -- the theory was computed
        Just th :: G_theory
th ->
         do
          -- display graph
          TaxoGraphKind -> String -> G_theory -> IO ()
displayGraph TaxoGraphKind
kind
                    (DGNodeLab -> String
getDGNodeName DGNodeLab
nlab) G_theory
th
          TaxoGraphKind -> CmdlState -> [LNode DGNodeLab] -> IO ()
taxoShowGeneric TaxoGraphKind
kind CmdlState
state [LNode DGNodeLab]
ll
        -- theory couldn't be computed so just go next
        _ -> TaxoGraphKind -> CmdlState -> [LNode DGNodeLab] -> IO ()
taxoShowGeneric TaxoGraphKind
kind CmdlState
state [LNode DGNodeLab]
ll
    _ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
#else
taxoShowGeneric _ _ _ = return ()
#endif

cShowTaxoGraph :: TaxoGraphKind -> String -> CmdlState -> IO CmdlState
cShowTaxoGraph :: TaxoGraphKind -> String -> CmdlState -> IO CmdlState
cShowTaxoGraph kind :: TaxoGraphKind
kind input :: String
input state :: CmdlState
state =
  case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
    Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state
    Just dgState :: IntIState
dgState ->
      do
        let (errors :: String
errors, nodes :: [LNode DGNodeLab]
nodes) = String -> IntIState -> (String, [LNode DGNodeLab])
getInputDGNodes String
input IntIState
dgState
        TaxoGraphKind -> CmdlState -> [LNode DGNodeLab] -> IO ()
taxoShowGeneric TaxoGraphKind
kind CmdlState
state [LNode DGNodeLab]
nodes
        CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlState -> CmdlState
genMessage String
errors [] CmdlState
state

cShowTaxonomy :: String -> CmdlState -> IO CmdlState
cShowTaxonomy :: String -> CmdlState -> IO CmdlState
cShowTaxonomy = TaxoGraphKind -> String -> CmdlState -> IO CmdlState
cShowTaxoGraph TaxoGraphKind
KSubsort

cShowConcept :: String -> CmdlState -> IO CmdlState
cShowConcept :: String -> CmdlState -> IO CmdlState
cShowConcept = TaxoGraphKind -> String -> CmdlState -> IO CmdlState
cShowTaxoGraph TaxoGraphKind
KConcept

-- show node number of input
cNodeNumber :: String -> CmdlState -> IO CmdlState
cNodeNumber :: String -> CmdlState -> IO CmdlState
cNodeNumber input :: String
input state :: CmdlState
state =
  case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
    Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state
    Just dgState :: IntIState
dgState ->
      let (errors :: String
errors, nodes :: [LNode DGNodeLab]
nodes) = String -> IntIState -> (String, [LNode DGNodeLab])
getInputDGNodes String
input IntIState
dgState
          ls :: [String]
ls = (LNode DGNodeLab -> String) -> [LNode DGNodeLab] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: Int
i, n :: DGNodeLab
n) -> DGNodeLab -> String
getDGNodeName DGNodeLab
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ " is node number " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                    Int -> String
forall a. Show a => a -> String
show Int
i) [LNode DGNodeLab]
nodes
       in CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlState -> CmdlState
genMessage String
errors (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" [String]
ls) CmdlState
state

-- print the name of all edges
cEdges :: CmdlState -> IO CmdlState
cEdges :: CmdlState -> IO CmdlState
cEdges state :: CmdlState
state
 = case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
    Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state
    Just dgState :: IntIState
dgState ->
     do
      -- list of all nodes
      let lsNodes :: [LNode DGNodeLab]
lsNodes = IntIState -> [LNode DGNodeLab]
getAllNodes IntIState
dgState
          -- compute all edges names
          lsEdg :: [LEdge DGLinkLab]
lsEdg = IntIState -> [LEdge DGLinkLab]
getAllEdges IntIState
dgState
          lsEdges :: [String]
lsEdges = ((String, LEdge DGLinkLab) -> String)
-> [(String, LEdge DGLinkLab)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, LEdge DGLinkLab) -> String
forall a b. (a, b) -> a
fst ([(String, LEdge DGLinkLab)] -> [String])
-> [(String, LEdge DGLinkLab)] -> [String]
forall a b. (a -> b) -> a -> b
$ [LNode DGNodeLab]
-> [LEdge DGLinkLab] -> [(String, LEdge DGLinkLab)]
createEdgeNames [LNode DGNodeLab]
lsNodes [LEdge DGLinkLab]
lsEdg
      -- print edge list in a sorted fashion
      CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlState -> CmdlState
genMessage [] (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. Ord a => [a] -> [a]
sort [String]
lsEdges) CmdlState
state

cUndoHistory :: CmdlState -> IO CmdlState
cUndoHistory :: CmdlState -> IO CmdlState
cUndoHistory = CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState)
-> (CmdlState -> CmdlState) -> CmdlState -> IO CmdlState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> CmdlState -> CmdlState
cHistory Bool
True

cRedoHistory :: CmdlState -> IO CmdlState
cRedoHistory :: CmdlState -> IO CmdlState
cRedoHistory = CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState)
-> (CmdlState -> CmdlState) -> CmdlState -> IO CmdlState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> CmdlState -> CmdlState
cHistory Bool
False

cCurrentComorphism :: CmdlState -> IO CmdlState
cCurrentComorphism :: CmdlState -> IO CmdlState
cCurrentComorphism st :: CmdlState
st =
 case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
st of
  Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlState -> CmdlState
genMessage "" "No comorphism!" CmdlState
st
  Just ist :: IntIState
ist -> case IntIState -> Maybe AnyComorphism
cComorphism IntIState
ist of
               Just cmor :: AnyComorphism
cmor -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlState -> CmdlState
genMessage "" (AnyComorphism -> String
forall a. Show a => a -> String
show AnyComorphism
cmor) CmdlState
st
               Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlState -> CmdlState
genMessage "" "No comorphism!" CmdlState
st

cHistory :: Bool -> CmdlState -> CmdlState
cHistory :: Bool -> CmdlState -> CmdlState
cHistory isUndo :: Bool
isUndo state :: CmdlState
state = String -> String -> CmdlState -> CmdlState
genMessage []
  ([String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((if Bool
isUndo then "Un" else "Re") String -> ShowS
forall a. [a] -> [a] -> [a]
++ "do history :")
    String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (CmdHistory -> String) -> [CmdHistory] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Command -> String
showCmd (Command -> String)
-> (CmdHistory -> Command) -> CmdHistory -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CmdHistory -> Command
command)
      ((if Bool
isUndo then IntHistory -> [CmdHistory]
undoList else IntHistory -> [CmdHistory]
redoList) (IntHistory -> [CmdHistory]) -> IntHistory -> [CmdHistory]
forall a b. (a -> b) -> a -> b
$ IntState -> IntHistory
i_hist (IntState -> IntHistory) -> IntState -> IntHistory
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state)
  ) CmdlState
state

-- print the name of all nodes
cNodes :: CmdlState -> IO CmdlState
cNodes :: CmdlState -> IO CmdlState
cNodes state :: CmdlState
state
 = case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
    -- no library loaded, so nothing to print
    Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state
    Just dgState :: IntIState
dgState ->
     do
     -- compute the list of node names
     let ls :: [String]
ls = [LNode DGNodeLab] -> [String]
forall a. [(a, DGNodeLab)] -> [String]
nodeNames ([LNode DGNodeLab] -> [String]) -> [LNode DGNodeLab] -> [String]
forall a b. (a -> b) -> a -> b
$ IntIState -> [LNode DGNodeLab]
getAllNodes IntIState
dgState
     -- print a sorted version of it
     CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlState -> CmdlState
genMessage [] (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. Ord a => [a] -> [a]
sort [String]
ls) CmdlState
state

cHelp :: [CmdlCmdDescription] -> CmdlState -> IO CmdlState
cHelp :: [CmdlCmdDescription] -> CmdlState -> IO CmdlState
cHelp allcmds :: [CmdlCmdDescription]
allcmds state :: CmdlState
state = do
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ (String, String, String) -> String
formatLine ("Command", "Parameter", "Description")
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
maxLineWidth '-'
  (CmdlCmdDescription -> IO ()) -> [CmdlCmdDescription] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ cm :: CmdlCmdDescription
cm -> do
                   let cmd :: Command
cmd = CmdlCmdDescription -> Command
cmdDescription CmdlCmdDescription
cm
                       name :: String
name = Command -> String
cmdNameStr Command
cmd
                       req :: String
req = CmdlCmdRequirements -> String
formatRequirement (CmdlCmdRequirements -> String) -> CmdlCmdRequirements -> String
forall a b. (a -> b) -> a -> b
$ CmdlCmdDescription -> CmdlCmdRequirements
cmdReq CmdlCmdDescription
cm
                       descL :: [String]
descL = String -> [String]
formatDesc (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ Command -> String
describeCmd Command
cmd
                       desc :: String
desc = [String] -> String
forall a. [a] -> a
head [String]
descL String -> ShowS
forall a. [a] -> [a] -> [a]
++
                              ShowS -> [String] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (('\n' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
descStart ' ') String -> ShowS
forall a. [a] -> [a] -> [a]
++)
                              ([String] -> [String]
forall a. [a] -> [a]
tail [String]
descL)
                   String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ (String, String, String) -> String
formatLine (String
name, String
req, String
desc)) [CmdlCmdDescription]
allcmds
  CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state
  where
    maxLineWidth :: Int
maxLineWidth = 80
    maxNameLen :: Int
maxNameLen = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (CmdlCmdDescription -> Int) -> [CmdlCmdDescription] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int)
-> (CmdlCmdDescription -> String) -> CmdlCmdDescription -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Command -> String
cmdNameStr (Command -> String)
-> (CmdlCmdDescription -> Command) -> CmdlCmdDescription -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CmdlCmdDescription -> Command
cmdDescription) [CmdlCmdDescription]
allcmds
    maxParamLen :: Int
maxParamLen = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (CmdlCmdDescription -> Int) -> [CmdlCmdDescription] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int)
-> (CmdlCmdDescription -> String) -> CmdlCmdDescription -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CmdlCmdRequirements -> String
formatRequirement (CmdlCmdRequirements -> String)
-> (CmdlCmdDescription -> CmdlCmdRequirements)
-> CmdlCmdDescription
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CmdlCmdDescription -> CmdlCmdRequirements
cmdReq ) [CmdlCmdDescription]
allcmds
    descStart :: Int
descStart = Int
maxNameLen Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
maxParamLen Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
    descWidth :: Int
descWidth = Int
maxLineWidth Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
descStart
    formatDesc :: String -> [String]
    formatDesc :: String -> [String]
formatDesc = [String] -> [String]
forall a. [a] -> [a]
reverse ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ShowS
trim ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                 ([String] -> String -> [String])
-> [String] -> [String] -> [String]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ l :: [String]
l w :: String
w -> if String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([String] -> String
forall a. [a] -> a
head [String]
l) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
w Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
descWidth
                                   then (String
w String -> ShowS
forall a. [a] -> [a] -> [a]
++ " ") String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
l
                                   else ([String] -> String
forall a. [a] -> a
head [String]
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
w String -> ShowS
forall a. [a] -> [a] -> [a]
++ " ") String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String] -> [String]
forall a. [a] -> [a]
tail [String]
l)
                       [""] ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
words
    formatLine :: (String, String, String) -> String
    formatLine :: (String, String, String) -> String
formatLine (c1 :: String
c1, c2 :: String
c2, c3 :: String
c3) =
      String
c1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
maxNameLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
c1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) ' ' String -> ShowS
forall a. [a] -> [a] -> [a]
++
      String
c2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
maxParamLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
c2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) ' ' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
c3