content: {- |
  Module      :  ./Interfaces/Command.hs
  Description :  development graph commands for all interfaces
  Copyright   :  (c) Christian Maeder, DFKI GmbH 2009
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  data types for development graph commands to be invoked via the GUI, the
  command-line-interface (CMDL), and other tools
  -}
  
  module Interfaces.Command where
  
  import Common.Utils
  
  import Data.Maybe
  import Data.Char
  import Data.List
  
  data GlobCmd =
      Automatic
    | GlobDecomp
    | GlobSubsume
    | LocalDecomp
    | LocalInference
    | CompositionProveEdges
    | CompositionCreateEdges
    | Conservativity
    | ThmHideShift
    | HideThmShift
    | Colimit
    | NormalForm
    | TriangleCons
    | Freeness
    | ThmFreeShift
    | QualifyNames
    | UndoCmd
    | RedoCmd
      -- Flattening command
    | Importing
    | DisjointUnion
    | Renaming
    | Hiding
    | Heterogeneity
    | ProveCurrent  -- CMDL prover activation
    | DisproveCurrent
    | CheckConsistencyCurrent
    | CheckConservativityAll
    | DropTranslation -- stop composing comorphisms to previous ones
      deriving (Eq, Ord, Enum, Bounded, Show)
  
  globCmdList :: [GlobCmd]
  globCmdList = [minBound .. maxBound]
  
  -- list of command names in the gui interface
  menuTextGlobCmd :: GlobCmd -> String
  menuTextGlobCmd cmd = case cmd of
    Automatic -> "Auto-DG-Prover"
    GlobDecomp -> "Global-Decomposition"
    GlobSubsume -> "Global-Subsumption"
    LocalDecomp -> "Local-Decomposition"
    LocalInference -> "Local-Inference"
    CompositionProveEdges -> "Prove composed edges"
    CompositionCreateEdges -> "Create composed proven edges"
    Conservativity -> "Conservativity"
    ThmHideShift -> "Theorem-Hide-Shift"
    ThmFreeShift -> "Theorem-Free-Shift"
    HideThmShift -> "Hide-Theorem-Shift"
    Colimit -> "Compute colimit"
    NormalForm -> "Compute normal form"
    TriangleCons -> "Triangle-Cons"
    QualifyNames -> "Qualify all names"
    UndoCmd -> "Undo"
    RedoCmd -> "Redo"
    Importing -> "Importing"
    DisjointUnion -> "Disjoint union"
    Renaming -> "Renaming"
    Hiding -> "Hiding"
    Freeness -> "Freeness"
    Heterogeneity -> "Heterogeneity"
    ProveCurrent -> "Prove"
    DisproveCurrent -> "Disprove"
    CheckConsistencyCurrent -> "Check consistency"
    CheckConservativityAll -> "Globally check conservativity"
    DropTranslation -> "Drop-Translations"
  
  -- | even some short names for the command line interface
  cmdlGlobCmd :: GlobCmd -> String
  cmdlGlobCmd cmd = case cmd of
    Automatic -> "auto"
    GlobDecomp -> "glob-decomp"
    GlobSubsume -> "global-subsume"
    LocalDecomp -> "loc-decomp"
    LocalInference -> "local-infer"
    CompositionProveEdges -> "comp"
    CompositionCreateEdges -> "comp-new"
    Conservativity -> "cons"
    ThmHideShift -> "thm-hide"
    HideThmShift -> "hide-thm"
    _ -> map (\ c -> if c == ' ' then '-' else toLower c) $ menuTextGlobCmd cmd
  
  isDgRule :: GlobCmd -> Bool
  isDgRule c = c <= HideThmShift
  
  isFlatteningCmd :: GlobCmd -> Bool
  isFlatteningCmd c = c >= Importing && c <= Heterogeneity
  
  isUndoOrRedo :: GlobCmd -> Bool
  isUndoOrRedo c = elem c [UndoCmd, RedoCmd]
  
  describeGlobCmd :: GlobCmd -> String
  describeGlobCmd c =
    let mt = menuTextGlobCmd c
        t = map toLower mt in
    case c of
    Automatic -> "Apply automatic tactic"
    CompositionProveEdges -> t
    CompositionCreateEdges -> t
    QualifyNames -> "Qualify and disambiguate all signature names"
    NormalForm -> "Compute normal forms for nodes with incoming hiding links"
    Importing -> "Flatten all theories and delete all importing links"
    DisjointUnion -> "Create intersection nodes and ensure only disjoint unions"
    Hiding -> "Delete all hiding links"
    ProveCurrent -> "Applies selected prover to selected goals"
    DropTranslation -> "Drops any selected comorphism"
    _ | isDgRule c -> "Apply rule " ++ t
      | isFlatteningCmd c -> "Flatten out " ++ t
      | isUndoOrRedo c -> mt ++ " last change"
    _ -> t
  
  globCmdNameStr :: GlobCmd -> String
  globCmdNameStr c = let s = cmdlGlobCmd c in
    if isDgRule c then "dg-all " ++ s else
    if isFlatteningCmd c then "flattening " ++ s else s
  
  -- | select a named entity
  data SelectCmd =
      LibFile -- read library from file
    | Lib  -- allows to move to an imported library
    | Node
    | ComorphismTranslation
    | Prover
    | Goal  -- a single goal for an automatic prover
    | ConsistencyChecker
    | Link
    | ConservativityCheckerOpen
    | ConservativityChecker
      deriving (Eq, Ord, Enum, Bounded, Show)
  
  selectCmdList :: [SelectCmd]
  selectCmdList = [minBound .. maxBound]
  
  selectCmdNameStr :: SelectCmd -> String
  selectCmdNameStr cmd = case cmd of
    LibFile -> "use"
    Lib -> "library"
    Node -> "dg basic"
    ComorphismTranslation -> "translate"
    Prover -> "prover"
    Goal -> "set goals"
    ConsistencyChecker -> "cons-checker"
    Link -> "link"
    ConservativityCheckerOpen -> "conservativity-check-open"
    ConservativityChecker -> "conservativity-check"
  
  describeSelectCmd :: SelectCmd -> String
  describeSelectCmd cmd = case cmd of
    LibFile -> "Read DOL file"
    Lib -> "Select library"
    Node -> "Select node"
    ComorphismTranslation -> "Choose translation"
    Prover -> "Choose prover"
    Goal -> "Set one or more space separated goal names"
    ConsistencyChecker -> "Choose consistency checker"
    Link -> "Select link"
    ConservativityChecker -> "Choose edges for a conservativity checker"
    ConservativityCheckerOpen -> "Choose open edges for a conservativity checker"
  
  data InspectCmd =
      Libs  -- all imported libraries
    | Nodes -- of library
    | Edges
    | UndoHist
    | RedoHist
    | EdgeInfo -- of a selected link
    | CurrentComorphism
    | LocalAxioms
    | NodeInfo
    | ComorphismsTo
    | TranslatedTheory
    | Theory
    | AllGoals
    | ProvenGoals
    | UnprovenGoals
    | Axioms
    | Taxonomy
    | Concept
      deriving (Eq, Ord, Enum, Bounded, Show)
  
  inspectCmdList :: [InspectCmd]
  inspectCmdList = [minBound .. maxBound]
  
  showInspectCmd :: InspectCmd -> String
  showInspectCmd cmd = case cmd of
    Libs -> "Library Names"
    Nodes -> "Nodes"
    Edges -> "Edges"
    ComorphismsTo -> "Comorphisms to"
    CurrentComorphism -> "Current Comorphism"
    TranslatedTheory -> "Translated Theory"
    UndoHist -> "Undo-History"
    RedoHist -> "Redo-History"
    EdgeInfo -> "Edge-Info"
    LocalAxioms -> "Local Axioms"
    NodeInfo -> "Node-Info"
    Theory -> "Computed Theory"
    AllGoals -> "All Goals"
    ProvenGoals -> "Proven Goals"
    UnprovenGoals -> "Unproven Goals"
    Axioms -> "All Axioms"
    Taxonomy -> "Taxonomy"
    Concept -> "Concept"
  
  requiresNode :: InspectCmd -> Bool
  requiresNode ic = ic >= LocalAxioms
  
  data ChangeCmd =
      Expand
    | AddView
      deriving (Eq, Ord, Enum, Bounded, Show)
  
  describeChangeCmd :: ChangeCmd -> String
  describeChangeCmd cmd = case cmd of
     Expand -> "Extend current node"
     AddView -> "Add a view"
  
  changeCmdList :: [ChangeCmd]
  changeCmdList = [minBound .. maxBound]
  
  changeCmdNameStr :: ChangeCmd -> String
  changeCmdNameStr cmd = case cmd of
    Expand -> "expand"
    AddView -> "addview"
  
  
  data Command =
      GlobCmd GlobCmd
    | SelectCmd SelectCmd String
    | TimeLimit Int -- set a time limit for an automatic  prover
    | SetAxioms [String] -- set the axiom list for an automatic  prover
    | ShowOutput Bool -- show model
    | IncludeProvenTheorems Bool -- should proven theorems be added as axioms
    | InspectCmd InspectCmd (Maybe String)
    | CommentCmd String
    | GroupCmd [Command] -- just to group commands in addCommandHistoryToState
    | ChangeCmd ChangeCmd String
    | HelpCmd
    | ExitCmd
    deriving (Show)
  
  -- the same command modulo input argument
  eqCmd :: Command -> Command -> Bool
  eqCmd c1 c2 = case (c1, c2) of
    (GlobCmd g1, GlobCmd g2) -> g1 == g2
    (SelectCmd s1 _, SelectCmd s2 _) -> s1 == s2
    (TimeLimit _, TimeLimit _) -> True
    (SetAxioms _, SetAxioms _) -> True
    (IncludeProvenTheorems b1, IncludeProvenTheorems b2) -> b1 == b2
    (InspectCmd i1 m1, InspectCmd i2 m2) -> i1 == i2 && isJust m1 == isJust m2
    (CommentCmd _, CommentCmd _) -> True
    (HelpCmd, HelpCmd) -> True
    (ExitCmd, ExitCmd) -> True
    (GroupCmd l1, GroupCmd l2) -> and (zipWith eqCmd l1 l2)
      && length l1 == length l2
    _ -> False
  
  mkSelectCmd :: SelectCmd -> Command
  mkSelectCmd s = SelectCmd s ""
  
  mkChangeCmd :: ChangeCmd -> Command
  mkChangeCmd c = ChangeCmd c ""
  
  cmdInputStr :: Command -> String
  cmdInputStr cmd = case cmd of
    SelectCmd _ t -> t
    TimeLimit l -> show l
    SetAxioms as -> unwords as
    InspectCmd _ t -> fromMaybe "" t
    ChangeCmd _ t -> t
    _ -> ""
  
  setInputStr :: String -> Command -> Command
  setInputStr str cmd = case cmd of
    SelectCmd s _ -> SelectCmd s str
    TimeLimit l -> TimeLimit $ case readMaybe str of
      Just n -> n
      _ -> l
    SetAxioms _ -> SetAxioms $ words str
    InspectCmd i _ -> InspectCmd i $ Just str
    ChangeCmd c _ -> ChangeCmd c str
    _ -> cmd
  
  cmdNameStr :: Command -> String
  cmdNameStr cmd = case cmd of
    GlobCmd g -> globCmdNameStr g
    SelectCmd s _ -> selectCmdNameStr s
    TimeLimit _ -> "set time-limit"
    SetAxioms _ -> "set axioms"
    ShowOutput b -> "show-output " ++ map toLower (show b)
    IncludeProvenTheorems b -> "set include-theorems " ++ map toLower (show b)
    InspectCmd i s ->
      (if i > Edges then "show-" else "")
      ++ map (\ c -> if c == ' ' then '-' else toLower c) (showInspectCmd i)
      ++ (if i > LocalAxioms && isNothing s && i /= ComorphismsTo
          then "-current" else "")
    CommentCmd _ -> "#"
    HelpCmd -> "help"
    ExitCmd -> "quit"
    GroupCmd _ -> ""
    ChangeCmd c _ -> changeCmdNameStr c
  
  -- | show command with arguments
  showCmd :: Command -> String
  showCmd c = let cn = cmdNameStr c in case c of
    SelectCmd _ t -> cn ++ " " ++ t
    TimeLimit l -> cn ++ " " ++ show l
    SetAxioms as -> unwords $ cn : as
    CommentCmd s -> cn ++ s
    GroupCmd l -> intercalate "\n" $ map showCmd l
    InspectCmd _ t -> cn ++ " " ++ fromMaybe "" t
    ChangeCmd _ t -> cmdNameStr c ++ " " ++ t
    ShowOutput b -> cn ++ show b
    _ -> cn
  
  describeCmd :: Command -> String
  describeCmd cmd = case cmd of
    GlobCmd g -> describeGlobCmd g
    SelectCmd s _ -> describeSelectCmd s
    TimeLimit _ -> "Set the time-limit for the next proof"
    SetAxioms _ -> "Set the axioms used for the next proof"
    ShowOutput b -> (if b then "S" else "Do not s")
      ++ "how model"
    IncludeProvenTheorems b -> (if b then "I" else "Do not i")
      ++ "nclude proven theorems"
    InspectCmd i t -> if i == ComorphismsTo
     then "Show comorphisms from currently selected node(s) to target logic"
     else "Show " ++ showInspectCmd i
      ++ (if i > LocalAxioms && isNothing t then " of selected node" else "")
    CommentCmd _ -> "Line comment"
    HelpCmd -> "Show all available commands"
    ExitCmd -> "Quit"
    GroupCmd _ -> "Grouping several commands"
    ChangeCmd c _ -> describeChangeCmd c
  
  commandList :: [Command]
  commandList =
    map GlobCmd globCmdList
    ++ map mkSelectCmd selectCmdList
    ++ [TimeLimit 0, SetAxioms []]
    ++ map IncludeProvenTheorems [False, True]
    ++ map (flip InspectCmd $ Just "") inspectCmdList
    ++ map (flip ChangeCmd "") changeCmdList
  
  {- unsafe commands are needed to
  delete or add
  Links, Nodes, Symbols from Signatures, and sentences
  
  A sequence of such unsafe operations should be checked by hets, if they will
  result in a consistent development graph, possibly indicating why not. -}
  