{- |
Module      :./CMDL/DataTypesUtils.hs
Description : utilitary functions used throughout the CMDL interface
Copyright   : uni-bremen and DFKI
License     : GPLv2 or higher, see LICENSE.txt
Maintainer  : r.pascanu@jacobs-university.de
Stability   : provisional
Portability : portable

CMDL.Utils contains different basic functions that are
used throughout the CMDL interface and could not be found in
Prelude

-}

module CMDL.DataTypesUtils
  ( getSelectedDGNodes
  , getCurrentSublogic
  , parseSublogics
  , getInputDGNodes
  , getInputNodes
  , getTh
  , baseChannels
  , genErrorMsg
  , genMessage
  , genAddMessage
  , generatePrompter
  , add2hist
  , getIdComorphism
  , resetErrorCode
  , genMsgAndCode
  , getExitCode
  , getExitCodeInt
  ) where

import Interfaces.Command (Command (CommentCmd))
import Interfaces.DataTypes
import Interfaces.History (add2history)
import Interfaces.Utils (getAllNodes)
import CMDL.Utils
import CMDL.DataTypes

import Static.GTheory (G_theory, mapG_theory, sublogicOfTh)
import Static.DevGraph (DGNodeLab (..), lookupDGraph, labDG)

import System.IO (stdout, stdin)
import System.Exit

import Proofs.AbstractState (sublogicOfTheory, theoryName)
import Static.ComputeTheory (computeTheory)

import Data.Graph.Inductive.Graph (LNode, Node)
import Data.List (find, break)
import Data.Map (lookup)

import Common.Result (Result (Result))

import Logic.Logic
import Logic.Comorphism (AnyComorphism (..), mkIdComorphism)
import Logic.Grothendieck (G_sublogics (..), joinSublogics, LogicGraph (logics))

import Comorphisms.LogicGraph (logicGraph)

add2hist :: [UndoRedoElem] -> CmdlState -> CmdlState
add2hist :: [UndoRedoElem] -> CmdlState -> CmdlState
add2hist descr :: [UndoRedoElem]
descr st :: CmdlState
st
 = let intst :: IntState
intst = Command -> IntState -> [UndoRedoElem] -> IntState
add2history (String -> Command
CommentCmd "") (CmdlState -> IntState
intState CmdlState
st) [UndoRedoElem]
descr
   in CmdlState
st { intState :: IntState
intState = IntState
intst }

{- | Given a list of selected theory generate an Id comorphism to the
first selected theory -}
getIdComorphism :: [Int_NodeInfo] -> Maybe AnyComorphism
getIdComorphism :: [Int_NodeInfo] -> Maybe AnyComorphism
getIdComorphism ls :: [Int_NodeInfo]
ls = case [Int_NodeInfo]
ls of
    [] -> Maybe AnyComorphism
forall a. Maybe a
Nothing
    Element st :: ProofState
st _ : _ ->
       case ProofState -> G_sublogics
sublogicOfTheory ProofState
st of
         G_sublogics lid :: lid
lid sub :: sublogics
sub -> AnyComorphism -> Maybe AnyComorphism
forall a. a -> Maybe a
Just (AnyComorphism -> Maybe AnyComorphism)
-> AnyComorphism -> Maybe AnyComorphism
forall a b. (a -> b) -> a -> b
$ InclComorphism lid sublogics -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism (lid -> sublogics -> InclComorphism lid sublogics
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 -> sublogics -> InclComorphism lid sublogics
mkIdComorphism lid
lid sublogics
sub)

-- | Generates the string containing the prompter
generatePrompter :: CmdlState -> String
generatePrompter :: CmdlState -> String
generatePrompter st :: CmdlState
st = let pst :: CmdlPrompterState
pst = CmdlState -> CmdlPrompterState
prompter CmdlState
st in
  (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 -> ""
    Just ist :: IntIState
ist ->
     let els :: String
els = case IntIState -> [Int_NodeInfo]
elements IntIState
ist of
                [] -> String -> String
delExtension (CmdlPrompterState -> String
fileLoaded CmdlPrompterState
pst)
                Element sm :: ProofState
sm _ : r :: [Int_NodeInfo]
r -> ProofState -> String
theoryName ProofState
sm String -> String -> String
forall a. [a] -> [a] -> [a]
++ if [Int_NodeInfo] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int_NodeInfo]
r then "" else ".."
         cm :: String
cm = case IntIState -> [Int_NodeInfo]
elements IntIState
ist of
                [] -> ""
                es :: [Int_NodeInfo]
es -> if IntIState -> Maybe AnyComorphism
cComorphism IntIState
ist Maybe AnyComorphism -> Maybe AnyComorphism -> Bool
forall a. Eq a => a -> a -> Bool
/= [Int_NodeInfo] -> Maybe AnyComorphism
getIdComorphism [Int_NodeInfo]
es
                       then "*"
                       else ""
     in String
els String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cm) String -> String -> String
forall a. [a] -> [a] -> [a]
++ CmdlPrompterState -> String
prompterHead CmdlPrompterState
pst

-- Returns the selected DGNodes along with a possible error message
getSelectedDGNodes :: IntIState -> (String, [LNode DGNodeLab])
getSelectedDGNodes :: IntIState -> (String, [LNode DGNodeLab])
getSelectedDGNodes dgState :: IntIState
dgState =
  let nds :: [Int]
nds = (Int_NodeInfo -> Int) -> [Int_NodeInfo] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Element _ n :: Int
n) -> Int
n) ([Int_NodeInfo] -> [Int]) -> [Int_NodeInfo] -> [Int]
forall a b. (a -> b) -> a -> b
$ IntIState -> [Int_NodeInfo]
elements IntIState
dgState
      dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph (IntIState -> LibName
i_ln IntIState
dgState) (IntIState -> LibEnv
i_libEnv IntIState
dgState)
      nds' :: [LNode DGNodeLab]
nds' = [Int] -> [DGNodeLab] -> [LNode DGNodeLab]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
nds ([DGNodeLab] -> [LNode DGNodeLab])
-> [DGNodeLab] -> [LNode DGNodeLab]
forall a b. (a -> b) -> a -> b
$ (Int -> DGNodeLab) -> [Int] -> [DGNodeLab]
forall a b. (a -> b) -> [a] -> [b]
map (DGraph -> Int -> DGNodeLab
labDG DGraph
dg) [Int]
nds
   in (if [LNode DGNodeLab] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LNode DGNodeLab]
nds' then "No node(s) selected!" else "", [LNode DGNodeLab]
nds')

getCurrentSublogic :: IntIState -> Maybe G_sublogics
getCurrentSublogic :: IntIState -> Maybe G_sublogics
getCurrentSublogic dgState :: IntIState
dgState =
 case IntIState -> (String, [LNode DGNodeLab])
getSelectedDGNodes IntIState
dgState of
  (_, []) -> Maybe G_sublogics
forall a. Maybe a
Nothing
  (_, ns :: [LNode DGNodeLab]
ns) -> case (LNode DGNodeLab -> G_sublogics)
-> [LNode DGNodeLab] -> [G_sublogics]
forall a b. (a -> b) -> [a] -> [b]
map (G_theory -> G_sublogics
sublogicOfTh (G_theory -> G_sublogics)
-> (LNode DGNodeLab -> G_theory) -> LNode DGNodeLab -> G_sublogics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGNodeLab -> G_theory
dgn_theory (DGNodeLab -> G_theory)
-> (LNode DGNodeLab -> DGNodeLab) -> LNode DGNodeLab -> G_theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LNode DGNodeLab -> DGNodeLab
forall a b. (a, b) -> b
snd) [LNode DGNodeLab]
ns of
             [] -> Maybe G_sublogics
forall a. Maybe a
Nothing
             sl1 :: G_sublogics
sl1 : sl' :: [G_sublogics]
sl' -> (Maybe G_sublogics -> G_sublogics -> Maybe G_sublogics)
-> Maybe G_sublogics -> [G_sublogics] -> Maybe G_sublogics
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((G_sublogics -> Maybe G_sublogics)
-> (G_sublogics -> G_sublogics -> Maybe G_sublogics)
-> Maybe G_sublogics
-> G_sublogics
-> Maybe G_sublogics
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Maybe G_sublogics -> G_sublogics -> Maybe G_sublogics
forall a b. a -> b -> a
const Maybe G_sublogics
forall a. Maybe a
Nothing) G_sublogics -> G_sublogics -> Maybe G_sublogics
joinSublogics)
                              (G_sublogics -> Maybe G_sublogics
forall a. a -> Maybe a
Just G_sublogics
sl1) [G_sublogics]
sl'

parseSublogics :: String -> Maybe G_sublogics
parseSublogics :: String -> Maybe G_sublogics
parseSublogics input :: String
input =
 if Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem '.' String
input then let (l :: String
l, _ : sl :: String
sl) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
Data.List.break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '.') String
input
                        in case String -> Map String AnyLogic -> Maybe AnyLogic
forall k a. Ord k => k -> Map k a -> Maybe a
Data.Map.lookup String
l (Map String AnyLogic -> Maybe AnyLogic)
-> Map String AnyLogic -> Maybe AnyLogic
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyLogic
logics LogicGraph
logicGraph of
                            Just (Logic lid :: lid
lid) ->
                             case lid -> String -> Maybe sublogics
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 -> String -> Maybe sublogics
parseSublogic lid
lid String
sl of
                              Just subl :: sublogics
subl -> G_sublogics -> Maybe G_sublogics
forall a. a -> Maybe a
Just (G_sublogics -> Maybe G_sublogics)
-> G_sublogics -> Maybe G_sublogics
forall a b. (a -> b) -> a -> b
$ lid -> sublogics -> G_sublogics
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 -> sublogics -> G_sublogics
G_sublogics lid
lid sublogics
subl
                              Nothing -> Maybe G_sublogics
forall a. Maybe a
Nothing
                            Nothing -> Maybe G_sublogics
forall a. Maybe a
Nothing
 else case String -> Map String AnyLogic -> Maybe AnyLogic
forall k a. Ord k => k -> Map k a -> Maybe a
Data.Map.lookup String
input (Map String AnyLogic -> Maybe AnyLogic)
-> Map String AnyLogic -> Maybe AnyLogic
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyLogic
logics LogicGraph
logicGraph of
       Just (Logic lid :: lid
lid) -> G_sublogics -> Maybe G_sublogics
forall a. a -> Maybe a
Just (G_sublogics -> Maybe G_sublogics)
-> G_sublogics -> Maybe G_sublogics
forall a b. (a -> b) -> a -> b
$ lid -> sublogics -> G_sublogics
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 -> sublogics -> G_sublogics
G_sublogics lid
lid (lid -> sublogics
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 -> sublogics
top_sublogic lid
lid)
       Nothing -> Maybe G_sublogics
forall a. Maybe a
Nothing

{- Returns the selected DGNodes
or if the selection is empty the DGNodes specified by the input string -}
getInputDGNodes :: String -> IntIState -> (String, [LNode DGNodeLab])
getInputDGNodes :: String -> IntIState -> (String, [LNode DGNodeLab])
getInputDGNodes input :: String
input dgState :: IntIState
dgState =
  if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
input
    then IntIState -> (String, [LNode DGNodeLab])
getSelectedDGNodes IntIState
dgState
    else let
        (nds :: [String]
nds, _, _, errs :: [String]
errs) = String -> ([String], [String], [String], [String])
decomposeIntoGoals String
input
        tmpErrs :: String
tmpErrs = [String] -> String
prettyPrintErrList [String]
errs
        in case [String]
nds of
               [] -> (String
tmpErrs, [])
               _ -> let
                   lsNodes :: [LNode DGNodeLab]
lsNodes = IntIState -> [LNode DGNodeLab]
getAllNodes IntIState
dgState
                   (errs' :: [String]
errs', listNodes :: [LNode DGNodeLab]
listNodes) = [String] -> [LNode DGNodeLab] -> ([String], [LNode DGNodeLab])
obtainNodeList [String]
nds [LNode DGNodeLab]
lsNodes
                   tmpErrs' :: String
tmpErrs' = String
tmpErrs String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
prettyPrintErrList [String]
errs'
                   in (String
tmpErrs', [LNode DGNodeLab]
listNodes)

{- Returns the selected Nodes
or if the selection is empty the Nodes specified by the input string -}
getInputNodes :: String -> IntIState -> (String, [Node])
getInputNodes :: String -> IntIState -> (String, [Int])
getInputNodes input :: String
input dgState :: IntIState
dgState =
  let (errors :: String
errors, nodes :: [LNode DGNodeLab]
nodes) = String -> IntIState -> (String, [LNode DGNodeLab])
getInputDGNodes String
input IntIState
dgState
   in (String
errors, (LNode DGNodeLab -> Int) -> [LNode DGNodeLab] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map LNode DGNodeLab -> Int
forall a b. (a, b) -> a
fst [LNode DGNodeLab]
nodes)

{- 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 -}
getTh :: CmdlUseTranslation -> Int -> CmdlState -> Maybe G_theory
getTh :: CmdlUseTranslation -> Int -> CmdlState -> Maybe G_theory
getTh useTrans :: CmdlUseTranslation
useTrans x :: Int
x st :: CmdlState
st
 = let
    -- compute the theory for a given node
       fn :: Int -> Maybe G_theory
fn n :: Int
n = 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 -> Maybe G_theory
forall a. Maybe a
Nothing
               Just ist :: IntIState
ist -> LibEnv -> LibName -> Int -> Maybe G_theory
computeTheory (IntIState -> LibEnv
i_libEnv IntIState
ist) (IntIState -> LibName
i_ln IntIState
ist) Int
n
   in
    case CmdlUseTranslation
useTrans of
     Dont_translate -> Int -> Maybe G_theory
fn Int
x
     Do_translate ->
      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 -> Maybe G_theory
forall a. Maybe a
Nothing
       Just ist :: IntIState
ist ->
        case IntIState -> [Int_NodeInfo]
elements IntIState
ist of
         [] -> Int -> Maybe G_theory
fn Int
x
         _ ->
          case (Int_NodeInfo -> Bool) -> [Int_NodeInfo] -> Maybe Int_NodeInfo
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\ y :: Int_NodeInfo
y -> case Int_NodeInfo
y of
                          Element _ z :: Int
z -> Int
z Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x) ([Int_NodeInfo] -> Maybe Int_NodeInfo)
-> [Int_NodeInfo] -> Maybe Int_NodeInfo
forall a b. (a -> b) -> a -> b
$
                  IntIState -> [Int_NodeInfo]
elements IntIState
ist of
           Nothing -> Int -> Maybe G_theory
fn Int
x
           Just _ ->
            case IntIState -> Maybe AnyComorphism
cComorphism IntIState
ist of
             Nothing -> Int -> Maybe G_theory
fn Int
x
             Just cm :: AnyComorphism
cm ->
              case Int -> Maybe G_theory
fn Int
x of
               Nothing -> Maybe G_theory
forall a. Maybe a
Nothing
               Just sth :: G_theory
sth ->
                case Bool -> AnyComorphism -> G_theory -> Result G_theory
mapG_theory Bool
False AnyComorphism
cm G_theory
sth of
                  Result _ Nothing -> G_theory -> Maybe G_theory
forall a. a -> Maybe a
Just G_theory
sth
                  Result _ (Just sth' :: G_theory
sth') -> G_theory -> Maybe G_theory
forall a. a -> Maybe a
Just G_theory
sth'


-- | Generates the base channels to be used (stdin and stdout)
baseChannels :: [CmdlChannel]
baseChannels :: [CmdlChannel]
baseChannels
 = let ch_in :: CmdlChannel
ch_in = CmdlChannel :: String
-> CmdlChannelType
-> Handle
-> Maybe CmdlSocket
-> CmdlChannelProperties
-> CmdlChannel
CmdlChannel {
                  chName :: String
chName = "stdin",
                  chType :: CmdlChannelType
chType = CmdlChannelType
ChStdin,
                  chHandler :: Handle
chHandler = Handle
stdin,
                  chSocket :: Maybe CmdlSocket
chSocket = Maybe CmdlSocket
forall a. Maybe a
Nothing,
                  chProperties :: CmdlChannelProperties
chProperties = CmdlChannelProperties
ChRead
                  }
       ch_out :: CmdlChannel
ch_out = CmdlChannel :: String
-> CmdlChannelType
-> Handle
-> Maybe CmdlSocket
-> CmdlChannelProperties
-> CmdlChannel
CmdlChannel {
                  chName :: String
chName = "stdout",
                  chType :: CmdlChannelType
chType = CmdlChannelType
ChStdout,
                  chHandler :: Handle
chHandler = Handle
stdout,
                  chSocket :: Maybe CmdlSocket
chSocket = Maybe CmdlSocket
forall a. Maybe a
Nothing,
                  chProperties :: CmdlChannelProperties
chProperties = CmdlChannelProperties
ChWrite
                  }
   in [CmdlChannel
ch_in, CmdlChannel
ch_out]

-- first changes the error code then generates a message
genMsgAndCode :: String -> Int -> CmdlState -> CmdlState
genMsgAndCode :: String -> Int -> CmdlState -> CmdlState
genMsgAndCode msg :: String
msg code :: Int
code st :: CmdlState
st = String -> CmdlState -> CmdlState
genErrorMsg String
msg (CmdlState
st {errorCode :: Int
errorCode = Int
code})


genErrorMsg :: String -> CmdlState -> CmdlState
genErrorMsg :: String -> CmdlState -> CmdlState
genErrorMsg msg :: String
msg st :: CmdlState
st
 = CmdlState
st {
      output :: CmdlMessage
output = CmdlMessage :: String -> String -> String -> CmdlMessage
CmdlMessage {
         outputMsg :: String
outputMsg = [],
         warningMsg :: String
warningMsg = [],
         errorMsg :: String
errorMsg = String
msg
         }
     }

genMessage :: String -> String -> CmdlState -> CmdlState
genMessage :: String -> String -> CmdlState -> CmdlState
genMessage warnings :: String
warnings msg :: String
msg st :: CmdlState
st
 = CmdlState
st {
        output :: CmdlMessage
output = CmdlMessage :: String -> String -> String -> CmdlMessage
CmdlMessage {
        outputMsg :: String
outputMsg = String
msg,
        warningMsg :: String
warningMsg = String
warnings,
        errorMsg :: String
errorMsg = []
        }
     }

genAddMessage :: String -> String -> CmdlState -> CmdlState
genAddMessage :: String -> String -> CmdlState -> CmdlState
genAddMessage warnings :: String
warnings msg :: String
msg st :: CmdlState
st = String -> String -> CmdlState -> CmdlState
genMessage String
warnings
 (case CmdlMessage -> String
outputMsg (CmdlMessage -> String) -> CmdlMessage -> String
forall a b. (a -> b) -> a -> b
$ CmdlState -> CmdlMessage
output CmdlState
st of
   "" -> String
msg
   msg1 :: String
msg1 -> String
msg1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg) CmdlState
st

resetErrorCode :: CmdlState -> CmdlState
resetErrorCode :: CmdlState -> CmdlState
resetErrorCode st :: CmdlState
st = CmdlState
st {errorCode :: Int
errorCode = 0}

getExitCode :: CmdlState -> ExitCode
getExitCode :: CmdlState -> ExitCode
getExitCode st :: CmdlState
st = if CmdlState -> Int
errorCode CmdlState
st Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then ExitCode
ExitSuccess
                                      else Int -> ExitCode
ExitFailure (Int -> ExitCode) -> Int -> ExitCode
forall a b. (a -> b) -> a -> b
$ CmdlState -> Int
errorCode CmdlState
st

getExitCodeInt :: CmdlState -> Int
getExitCodeInt :: CmdlState -> Int
getExitCodeInt = CmdlState -> Int
errorCode