{- |
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. -}