{- |
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 (GlobCmd -> GlobCmd -> Bool
(GlobCmd -> GlobCmd -> Bool)
-> (GlobCmd -> GlobCmd -> Bool) -> Eq GlobCmd
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GlobCmd -> GlobCmd -> Bool
$c/= :: GlobCmd -> GlobCmd -> Bool
== :: GlobCmd -> GlobCmd -> Bool
$c== :: GlobCmd -> GlobCmd -> Bool
Eq, Eq GlobCmd
Eq GlobCmd =>
(GlobCmd -> GlobCmd -> Ordering)
-> (GlobCmd -> GlobCmd -> Bool)
-> (GlobCmd -> GlobCmd -> Bool)
-> (GlobCmd -> GlobCmd -> Bool)
-> (GlobCmd -> GlobCmd -> Bool)
-> (GlobCmd -> GlobCmd -> GlobCmd)
-> (GlobCmd -> GlobCmd -> GlobCmd)
-> Ord GlobCmd
GlobCmd -> GlobCmd -> Bool
GlobCmd -> GlobCmd -> Ordering
GlobCmd -> GlobCmd -> GlobCmd
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: GlobCmd -> GlobCmd -> GlobCmd
$cmin :: GlobCmd -> GlobCmd -> GlobCmd
max :: GlobCmd -> GlobCmd -> GlobCmd
$cmax :: GlobCmd -> GlobCmd -> GlobCmd
>= :: GlobCmd -> GlobCmd -> Bool
$c>= :: GlobCmd -> GlobCmd -> Bool
> :: GlobCmd -> GlobCmd -> Bool
$c> :: GlobCmd -> GlobCmd -> Bool
<= :: GlobCmd -> GlobCmd -> Bool
$c<= :: GlobCmd -> GlobCmd -> Bool
< :: GlobCmd -> GlobCmd -> Bool
$c< :: GlobCmd -> GlobCmd -> Bool
compare :: GlobCmd -> GlobCmd -> Ordering
$ccompare :: GlobCmd -> GlobCmd -> Ordering
$cp1Ord :: Eq GlobCmd
Ord, Int -> GlobCmd
GlobCmd -> Int
GlobCmd -> [GlobCmd]
GlobCmd -> GlobCmd
GlobCmd -> GlobCmd -> [GlobCmd]
GlobCmd -> GlobCmd -> GlobCmd -> [GlobCmd]
(GlobCmd -> GlobCmd)
-> (GlobCmd -> GlobCmd)
-> (Int -> GlobCmd)
-> (GlobCmd -> Int)
-> (GlobCmd -> [GlobCmd])
-> (GlobCmd -> GlobCmd -> [GlobCmd])
-> (GlobCmd -> GlobCmd -> [GlobCmd])
-> (GlobCmd -> GlobCmd -> GlobCmd -> [GlobCmd])
-> Enum GlobCmd
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: GlobCmd -> GlobCmd -> GlobCmd -> [GlobCmd]
$cenumFromThenTo :: GlobCmd -> GlobCmd -> GlobCmd -> [GlobCmd]
enumFromTo :: GlobCmd -> GlobCmd -> [GlobCmd]
$cenumFromTo :: GlobCmd -> GlobCmd -> [GlobCmd]
enumFromThen :: GlobCmd -> GlobCmd -> [GlobCmd]
$cenumFromThen :: GlobCmd -> GlobCmd -> [GlobCmd]
enumFrom :: GlobCmd -> [GlobCmd]
$cenumFrom :: GlobCmd -> [GlobCmd]
fromEnum :: GlobCmd -> Int
$cfromEnum :: GlobCmd -> Int
toEnum :: Int -> GlobCmd
$ctoEnum :: Int -> GlobCmd
pred :: GlobCmd -> GlobCmd
$cpred :: GlobCmd -> GlobCmd
succ :: GlobCmd -> GlobCmd
$csucc :: GlobCmd -> GlobCmd
Enum, GlobCmd
GlobCmd -> GlobCmd -> Bounded GlobCmd
forall a. a -> a -> Bounded a
maxBound :: GlobCmd
$cmaxBound :: GlobCmd
minBound :: GlobCmd
$cminBound :: GlobCmd
Bounded, Int -> GlobCmd -> ShowS
[GlobCmd] -> ShowS
GlobCmd -> String
(Int -> GlobCmd -> ShowS)
-> (GlobCmd -> String) -> ([GlobCmd] -> ShowS) -> Show GlobCmd
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GlobCmd] -> ShowS
$cshowList :: [GlobCmd] -> ShowS
show :: GlobCmd -> String
$cshow :: GlobCmd -> String
showsPrec :: Int -> GlobCmd -> ShowS
$cshowsPrec :: Int -> GlobCmd -> ShowS
Show)

globCmdList :: [GlobCmd]
globCmdList :: [GlobCmd]
globCmdList = [GlobCmd
forall a. Bounded a => a
minBound .. GlobCmd
forall a. Bounded a => a
maxBound]

-- list of command names in the gui interface
menuTextGlobCmd :: GlobCmd -> String
menuTextGlobCmd :: GlobCmd -> String
menuTextGlobCmd cmd :: GlobCmd
cmd = case GlobCmd
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 :: GlobCmd -> String
cmdlGlobCmd cmd :: GlobCmd
cmd = case GlobCmd
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"
  _ -> (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map (\ c :: Char
c -> if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== ' ' then '-' else Char -> Char
toLower Char
c) ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ GlobCmd -> String
menuTextGlobCmd GlobCmd
cmd

isDgRule :: GlobCmd -> Bool
isDgRule :: GlobCmd -> Bool
isDgRule c :: GlobCmd
c = GlobCmd
c GlobCmd -> GlobCmd -> Bool
forall a. Ord a => a -> a -> Bool
<= GlobCmd
HideThmShift

isFlatteningCmd :: GlobCmd -> Bool
isFlatteningCmd :: GlobCmd -> Bool
isFlatteningCmd c :: GlobCmd
c = GlobCmd
c GlobCmd -> GlobCmd -> Bool
forall a. Ord a => a -> a -> Bool
>= GlobCmd
Importing Bool -> Bool -> Bool
&& GlobCmd
c GlobCmd -> GlobCmd -> Bool
forall a. Ord a => a -> a -> Bool
<= GlobCmd
Heterogeneity

isUndoOrRedo :: GlobCmd -> Bool
isUndoOrRedo :: GlobCmd -> Bool
isUndoOrRedo c :: GlobCmd
c = GlobCmd -> [GlobCmd] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem GlobCmd
c [GlobCmd
UndoCmd, GlobCmd
RedoCmd]

describeGlobCmd :: GlobCmd -> String
describeGlobCmd :: GlobCmd -> String
describeGlobCmd c :: GlobCmd
c =
  let mt :: String
mt = GlobCmd -> String
menuTextGlobCmd GlobCmd
c
      t :: String
t = (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
mt in
  case GlobCmd
c of
  Automatic -> "Apply automatic tactic"
  CompositionProveEdges -> String
t
  CompositionCreateEdges -> String
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"
  _ | GlobCmd -> Bool
isDgRule GlobCmd
c -> "Apply rule " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
t
    | GlobCmd -> Bool
isFlatteningCmd GlobCmd
c -> "Flatten out " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
t
    | GlobCmd -> Bool
isUndoOrRedo GlobCmd
c -> String
mt String -> ShowS
forall a. [a] -> [a] -> [a]
++ " last change"
  _ -> String
t

globCmdNameStr :: GlobCmd -> String
globCmdNameStr :: GlobCmd -> String
globCmdNameStr c :: GlobCmd
c = let s :: String
s = GlobCmd -> String
cmdlGlobCmd GlobCmd
c in
  if GlobCmd -> Bool
isDgRule GlobCmd
c then "dg-all " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s else
  if GlobCmd -> Bool
isFlatteningCmd GlobCmd
c then "flattening " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s else String
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 (SelectCmd -> SelectCmd -> Bool
(SelectCmd -> SelectCmd -> Bool)
-> (SelectCmd -> SelectCmd -> Bool) -> Eq SelectCmd
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SelectCmd -> SelectCmd -> Bool
$c/= :: SelectCmd -> SelectCmd -> Bool
== :: SelectCmd -> SelectCmd -> Bool
$c== :: SelectCmd -> SelectCmd -> Bool
Eq, Eq SelectCmd
Eq SelectCmd =>
(SelectCmd -> SelectCmd -> Ordering)
-> (SelectCmd -> SelectCmd -> Bool)
-> (SelectCmd -> SelectCmd -> Bool)
-> (SelectCmd -> SelectCmd -> Bool)
-> (SelectCmd -> SelectCmd -> Bool)
-> (SelectCmd -> SelectCmd -> SelectCmd)
-> (SelectCmd -> SelectCmd -> SelectCmd)
-> Ord SelectCmd
SelectCmd -> SelectCmd -> Bool
SelectCmd -> SelectCmd -> Ordering
SelectCmd -> SelectCmd -> SelectCmd
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SelectCmd -> SelectCmd -> SelectCmd
$cmin :: SelectCmd -> SelectCmd -> SelectCmd
max :: SelectCmd -> SelectCmd -> SelectCmd
$cmax :: SelectCmd -> SelectCmd -> SelectCmd
>= :: SelectCmd -> SelectCmd -> Bool
$c>= :: SelectCmd -> SelectCmd -> Bool
> :: SelectCmd -> SelectCmd -> Bool
$c> :: SelectCmd -> SelectCmd -> Bool
<= :: SelectCmd -> SelectCmd -> Bool
$c<= :: SelectCmd -> SelectCmd -> Bool
< :: SelectCmd -> SelectCmd -> Bool
$c< :: SelectCmd -> SelectCmd -> Bool
compare :: SelectCmd -> SelectCmd -> Ordering
$ccompare :: SelectCmd -> SelectCmd -> Ordering
$cp1Ord :: Eq SelectCmd
Ord, Int -> SelectCmd
SelectCmd -> Int
SelectCmd -> [SelectCmd]
SelectCmd -> SelectCmd
SelectCmd -> SelectCmd -> [SelectCmd]
SelectCmd -> SelectCmd -> SelectCmd -> [SelectCmd]
(SelectCmd -> SelectCmd)
-> (SelectCmd -> SelectCmd)
-> (Int -> SelectCmd)
-> (SelectCmd -> Int)
-> (SelectCmd -> [SelectCmd])
-> (SelectCmd -> SelectCmd -> [SelectCmd])
-> (SelectCmd -> SelectCmd -> [SelectCmd])
-> (SelectCmd -> SelectCmd -> SelectCmd -> [SelectCmd])
-> Enum SelectCmd
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: SelectCmd -> SelectCmd -> SelectCmd -> [SelectCmd]
$cenumFromThenTo :: SelectCmd -> SelectCmd -> SelectCmd -> [SelectCmd]
enumFromTo :: SelectCmd -> SelectCmd -> [SelectCmd]
$cenumFromTo :: SelectCmd -> SelectCmd -> [SelectCmd]
enumFromThen :: SelectCmd -> SelectCmd -> [SelectCmd]
$cenumFromThen :: SelectCmd -> SelectCmd -> [SelectCmd]
enumFrom :: SelectCmd -> [SelectCmd]
$cenumFrom :: SelectCmd -> [SelectCmd]
fromEnum :: SelectCmd -> Int
$cfromEnum :: SelectCmd -> Int
toEnum :: Int -> SelectCmd
$ctoEnum :: Int -> SelectCmd
pred :: SelectCmd -> SelectCmd
$cpred :: SelectCmd -> SelectCmd
succ :: SelectCmd -> SelectCmd
$csucc :: SelectCmd -> SelectCmd
Enum, SelectCmd
SelectCmd -> SelectCmd -> Bounded SelectCmd
forall a. a -> a -> Bounded a
maxBound :: SelectCmd
$cmaxBound :: SelectCmd
minBound :: SelectCmd
$cminBound :: SelectCmd
Bounded, Int -> SelectCmd -> ShowS
[SelectCmd] -> ShowS
SelectCmd -> String
(Int -> SelectCmd -> ShowS)
-> (SelectCmd -> String)
-> ([SelectCmd] -> ShowS)
-> Show SelectCmd
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SelectCmd] -> ShowS
$cshowList :: [SelectCmd] -> ShowS
show :: SelectCmd -> String
$cshow :: SelectCmd -> String
showsPrec :: Int -> SelectCmd -> ShowS
$cshowsPrec :: Int -> SelectCmd -> ShowS
Show)

selectCmdList :: [SelectCmd]
selectCmdList :: [SelectCmd]
selectCmdList = [SelectCmd
forall a. Bounded a => a
minBound .. SelectCmd
forall a. Bounded a => a
maxBound]

selectCmdNameStr :: SelectCmd -> String
selectCmdNameStr :: SelectCmd -> String
selectCmdNameStr cmd :: SelectCmd
cmd = case SelectCmd
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 :: SelectCmd -> String
describeSelectCmd cmd :: SelectCmd
cmd = case SelectCmd
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 (InspectCmd -> InspectCmd -> Bool
(InspectCmd -> InspectCmd -> Bool)
-> (InspectCmd -> InspectCmd -> Bool) -> Eq InspectCmd
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: InspectCmd -> InspectCmd -> Bool
$c/= :: InspectCmd -> InspectCmd -> Bool
== :: InspectCmd -> InspectCmd -> Bool
$c== :: InspectCmd -> InspectCmd -> Bool
Eq, Eq InspectCmd
Eq InspectCmd =>
(InspectCmd -> InspectCmd -> Ordering)
-> (InspectCmd -> InspectCmd -> Bool)
-> (InspectCmd -> InspectCmd -> Bool)
-> (InspectCmd -> InspectCmd -> Bool)
-> (InspectCmd -> InspectCmd -> Bool)
-> (InspectCmd -> InspectCmd -> InspectCmd)
-> (InspectCmd -> InspectCmd -> InspectCmd)
-> Ord InspectCmd
InspectCmd -> InspectCmd -> Bool
InspectCmd -> InspectCmd -> Ordering
InspectCmd -> InspectCmd -> InspectCmd
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: InspectCmd -> InspectCmd -> InspectCmd
$cmin :: InspectCmd -> InspectCmd -> InspectCmd
max :: InspectCmd -> InspectCmd -> InspectCmd
$cmax :: InspectCmd -> InspectCmd -> InspectCmd
>= :: InspectCmd -> InspectCmd -> Bool
$c>= :: InspectCmd -> InspectCmd -> Bool
> :: InspectCmd -> InspectCmd -> Bool
$c> :: InspectCmd -> InspectCmd -> Bool
<= :: InspectCmd -> InspectCmd -> Bool
$c<= :: InspectCmd -> InspectCmd -> Bool
< :: InspectCmd -> InspectCmd -> Bool
$c< :: InspectCmd -> InspectCmd -> Bool
compare :: InspectCmd -> InspectCmd -> Ordering
$ccompare :: InspectCmd -> InspectCmd -> Ordering
$cp1Ord :: Eq InspectCmd
Ord, Int -> InspectCmd
InspectCmd -> Int
InspectCmd -> [InspectCmd]
InspectCmd -> InspectCmd
InspectCmd -> InspectCmd -> [InspectCmd]
InspectCmd -> InspectCmd -> InspectCmd -> [InspectCmd]
(InspectCmd -> InspectCmd)
-> (InspectCmd -> InspectCmd)
-> (Int -> InspectCmd)
-> (InspectCmd -> Int)
-> (InspectCmd -> [InspectCmd])
-> (InspectCmd -> InspectCmd -> [InspectCmd])
-> (InspectCmd -> InspectCmd -> [InspectCmd])
-> (InspectCmd -> InspectCmd -> InspectCmd -> [InspectCmd])
-> Enum InspectCmd
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: InspectCmd -> InspectCmd -> InspectCmd -> [InspectCmd]
$cenumFromThenTo :: InspectCmd -> InspectCmd -> InspectCmd -> [InspectCmd]
enumFromTo :: InspectCmd -> InspectCmd -> [InspectCmd]
$cenumFromTo :: InspectCmd -> InspectCmd -> [InspectCmd]
enumFromThen :: InspectCmd -> InspectCmd -> [InspectCmd]
$cenumFromThen :: InspectCmd -> InspectCmd -> [InspectCmd]
enumFrom :: InspectCmd -> [InspectCmd]
$cenumFrom :: InspectCmd -> [InspectCmd]
fromEnum :: InspectCmd -> Int
$cfromEnum :: InspectCmd -> Int
toEnum :: Int -> InspectCmd
$ctoEnum :: Int -> InspectCmd
pred :: InspectCmd -> InspectCmd
$cpred :: InspectCmd -> InspectCmd
succ :: InspectCmd -> InspectCmd
$csucc :: InspectCmd -> InspectCmd
Enum, InspectCmd
InspectCmd -> InspectCmd -> Bounded InspectCmd
forall a. a -> a -> Bounded a
maxBound :: InspectCmd
$cmaxBound :: InspectCmd
minBound :: InspectCmd
$cminBound :: InspectCmd
Bounded, Int -> InspectCmd -> ShowS
[InspectCmd] -> ShowS
InspectCmd -> String
(Int -> InspectCmd -> ShowS)
-> (InspectCmd -> String)
-> ([InspectCmd] -> ShowS)
-> Show InspectCmd
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [InspectCmd] -> ShowS
$cshowList :: [InspectCmd] -> ShowS
show :: InspectCmd -> String
$cshow :: InspectCmd -> String
showsPrec :: Int -> InspectCmd -> ShowS
$cshowsPrec :: Int -> InspectCmd -> ShowS
Show)

inspectCmdList :: [InspectCmd]
inspectCmdList :: [InspectCmd]
inspectCmdList = [InspectCmd
forall a. Bounded a => a
minBound .. InspectCmd
forall a. Bounded a => a
maxBound]

showInspectCmd :: InspectCmd -> String
showInspectCmd :: InspectCmd -> String
showInspectCmd cmd :: InspectCmd
cmd = case InspectCmd
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 :: InspectCmd -> Bool
requiresNode ic :: InspectCmd
ic = InspectCmd
ic InspectCmd -> InspectCmd -> Bool
forall a. Ord a => a -> a -> Bool
>= InspectCmd
LocalAxioms

data ChangeCmd =
    Expand
  | AddView
    deriving (ChangeCmd -> ChangeCmd -> Bool
(ChangeCmd -> ChangeCmd -> Bool)
-> (ChangeCmd -> ChangeCmd -> Bool) -> Eq ChangeCmd
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ChangeCmd -> ChangeCmd -> Bool
$c/= :: ChangeCmd -> ChangeCmd -> Bool
== :: ChangeCmd -> ChangeCmd -> Bool
$c== :: ChangeCmd -> ChangeCmd -> Bool
Eq, Eq ChangeCmd
Eq ChangeCmd =>
(ChangeCmd -> ChangeCmd -> Ordering)
-> (ChangeCmd -> ChangeCmd -> Bool)
-> (ChangeCmd -> ChangeCmd -> Bool)
-> (ChangeCmd -> ChangeCmd -> Bool)
-> (ChangeCmd -> ChangeCmd -> Bool)
-> (ChangeCmd -> ChangeCmd -> ChangeCmd)
-> (ChangeCmd -> ChangeCmd -> ChangeCmd)
-> Ord ChangeCmd
ChangeCmd -> ChangeCmd -> Bool
ChangeCmd -> ChangeCmd -> Ordering
ChangeCmd -> ChangeCmd -> ChangeCmd
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ChangeCmd -> ChangeCmd -> ChangeCmd
$cmin :: ChangeCmd -> ChangeCmd -> ChangeCmd
max :: ChangeCmd -> ChangeCmd -> ChangeCmd
$cmax :: ChangeCmd -> ChangeCmd -> ChangeCmd
>= :: ChangeCmd -> ChangeCmd -> Bool
$c>= :: ChangeCmd -> ChangeCmd -> Bool
> :: ChangeCmd -> ChangeCmd -> Bool
$c> :: ChangeCmd -> ChangeCmd -> Bool
<= :: ChangeCmd -> ChangeCmd -> Bool
$c<= :: ChangeCmd -> ChangeCmd -> Bool
< :: ChangeCmd -> ChangeCmd -> Bool
$c< :: ChangeCmd -> ChangeCmd -> Bool
compare :: ChangeCmd -> ChangeCmd -> Ordering
$ccompare :: ChangeCmd -> ChangeCmd -> Ordering
$cp1Ord :: Eq ChangeCmd
Ord, Int -> ChangeCmd
ChangeCmd -> Int
ChangeCmd -> [ChangeCmd]
ChangeCmd -> ChangeCmd
ChangeCmd -> ChangeCmd -> [ChangeCmd]
ChangeCmd -> ChangeCmd -> ChangeCmd -> [ChangeCmd]
(ChangeCmd -> ChangeCmd)
-> (ChangeCmd -> ChangeCmd)
-> (Int -> ChangeCmd)
-> (ChangeCmd -> Int)
-> (ChangeCmd -> [ChangeCmd])
-> (ChangeCmd -> ChangeCmd -> [ChangeCmd])
-> (ChangeCmd -> ChangeCmd -> [ChangeCmd])
-> (ChangeCmd -> ChangeCmd -> ChangeCmd -> [ChangeCmd])
-> Enum ChangeCmd
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: ChangeCmd -> ChangeCmd -> ChangeCmd -> [ChangeCmd]
$cenumFromThenTo :: ChangeCmd -> ChangeCmd -> ChangeCmd -> [ChangeCmd]
enumFromTo :: ChangeCmd -> ChangeCmd -> [ChangeCmd]
$cenumFromTo :: ChangeCmd -> ChangeCmd -> [ChangeCmd]
enumFromThen :: ChangeCmd -> ChangeCmd -> [ChangeCmd]
$cenumFromThen :: ChangeCmd -> ChangeCmd -> [ChangeCmd]
enumFrom :: ChangeCmd -> [ChangeCmd]
$cenumFrom :: ChangeCmd -> [ChangeCmd]
fromEnum :: ChangeCmd -> Int
$cfromEnum :: ChangeCmd -> Int
toEnum :: Int -> ChangeCmd
$ctoEnum :: Int -> ChangeCmd
pred :: ChangeCmd -> ChangeCmd
$cpred :: ChangeCmd -> ChangeCmd
succ :: ChangeCmd -> ChangeCmd
$csucc :: ChangeCmd -> ChangeCmd
Enum, ChangeCmd
ChangeCmd -> ChangeCmd -> Bounded ChangeCmd
forall a. a -> a -> Bounded a
maxBound :: ChangeCmd
$cmaxBound :: ChangeCmd
minBound :: ChangeCmd
$cminBound :: ChangeCmd
Bounded, Int -> ChangeCmd -> ShowS
[ChangeCmd] -> ShowS
ChangeCmd -> String
(Int -> ChangeCmd -> ShowS)
-> (ChangeCmd -> String)
-> ([ChangeCmd] -> ShowS)
-> Show ChangeCmd
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ChangeCmd] -> ShowS
$cshowList :: [ChangeCmd] -> ShowS
show :: ChangeCmd -> String
$cshow :: ChangeCmd -> String
showsPrec :: Int -> ChangeCmd -> ShowS
$cshowsPrec :: Int -> ChangeCmd -> ShowS
Show)

describeChangeCmd :: ChangeCmd -> String
describeChangeCmd :: ChangeCmd -> String
describeChangeCmd cmd :: ChangeCmd
cmd = case ChangeCmd
cmd of
   Expand -> "Extend current node"
   AddView -> "Add a view"

changeCmdList :: [ChangeCmd]
changeCmdList :: [ChangeCmd]
changeCmdList = [ChangeCmd
forall a. Bounded a => a
minBound .. ChangeCmd
forall a. Bounded a => a
maxBound]

changeCmdNameStr :: ChangeCmd -> String
changeCmdNameStr :: ChangeCmd -> String
changeCmdNameStr cmd :: ChangeCmd
cmd = case ChangeCmd
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 (Int -> Command -> ShowS
[Command] -> ShowS
Command -> String
(Int -> Command -> ShowS)
-> (Command -> String) -> ([Command] -> ShowS) -> Show Command
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Command] -> ShowS
$cshowList :: [Command] -> ShowS
show :: Command -> String
$cshow :: Command -> String
showsPrec :: Int -> Command -> ShowS
$cshowsPrec :: Int -> Command -> ShowS
Show)

-- the same command modulo input argument
eqCmd :: Command -> Command -> Bool
eqCmd :: Command -> Command -> Bool
eqCmd c1 :: Command
c1 c2 :: Command
c2 = case (Command
c1, Command
c2) of
  (GlobCmd g1 :: GlobCmd
g1, GlobCmd g2 :: GlobCmd
g2) -> GlobCmd
g1 GlobCmd -> GlobCmd -> Bool
forall a. Eq a => a -> a -> Bool
== GlobCmd
g2
  (SelectCmd s1 :: SelectCmd
s1 _, SelectCmd s2 :: SelectCmd
s2 _) -> SelectCmd
s1 SelectCmd -> SelectCmd -> Bool
forall a. Eq a => a -> a -> Bool
== SelectCmd
s2
  (TimeLimit _, TimeLimit _) -> Bool
True
  (SetAxioms _, SetAxioms _) -> Bool
True
  (IncludeProvenTheorems b1 :: Bool
b1, IncludeProvenTheorems b2 :: Bool
b2) -> Bool
b1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b2
  (InspectCmd i1 :: InspectCmd
i1 m1 :: Maybe String
m1, InspectCmd i2 :: InspectCmd
i2 m2 :: Maybe String
m2) -> InspectCmd
i1 InspectCmd -> InspectCmd -> Bool
forall a. Eq a => a -> a -> Bool
== InspectCmd
i2 Bool -> Bool -> Bool
&& Maybe String -> Bool
forall a. Maybe a -> Bool
isJust Maybe String
m1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe String -> Bool
forall a. Maybe a -> Bool
isJust Maybe String
m2
  (CommentCmd _, CommentCmd _) -> Bool
True
  (HelpCmd, HelpCmd) -> Bool
True
  (ExitCmd, ExitCmd) -> Bool
True
  (GroupCmd l1 :: [Command]
l1, GroupCmd l2 :: [Command]
l2) -> [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Command -> Command -> Bool) -> [Command] -> [Command] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Command -> Command -> Bool
eqCmd [Command]
l1 [Command]
l2)
    Bool -> Bool -> Bool
&& [Command] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Command]
l1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Command] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Command]
l2
  _ -> Bool
False

mkSelectCmd :: SelectCmd -> Command
mkSelectCmd :: SelectCmd -> Command
mkSelectCmd s :: SelectCmd
s = SelectCmd -> String -> Command
SelectCmd SelectCmd
s ""

mkChangeCmd :: ChangeCmd -> Command
mkChangeCmd :: ChangeCmd -> Command
mkChangeCmd c :: ChangeCmd
c = ChangeCmd -> String -> Command
ChangeCmd ChangeCmd
c ""

cmdInputStr :: Command -> String
cmdInputStr :: Command -> String
cmdInputStr cmd :: Command
cmd = case Command
cmd of
  SelectCmd _ t :: String
t -> String
t
  TimeLimit l :: Int
l -> Int -> String
forall a. Show a => a -> String
show Int
l
  SetAxioms as :: [String]
as -> [String] -> String
unwords [String]
as
  InspectCmd _ t :: Maybe String
t -> String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "" Maybe String
t
  ChangeCmd _ t :: String
t -> String
t
  _ -> ""

setInputStr :: String -> Command -> Command
setInputStr :: String -> Command -> Command
setInputStr str :: String
str cmd :: Command
cmd = case Command
cmd of
  SelectCmd s :: SelectCmd
s _ -> SelectCmd -> String -> Command
SelectCmd SelectCmd
s String
str
  TimeLimit l :: Int
l -> Int -> Command
TimeLimit (Int -> Command) -> Int -> Command
forall a b. (a -> b) -> a -> b
$ case String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe String
str of
    Just n :: Int
n -> Int
n
    _ -> Int
l
  SetAxioms _ -> [String] -> Command
SetAxioms ([String] -> Command) -> [String] -> Command
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
str
  InspectCmd i :: InspectCmd
i _ -> InspectCmd -> Maybe String -> Command
InspectCmd InspectCmd
i (Maybe String -> Command) -> Maybe String -> Command
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
str
  ChangeCmd c :: ChangeCmd
c _ -> ChangeCmd -> String -> Command
ChangeCmd ChangeCmd
c String
str
  _ -> Command
cmd

cmdNameStr :: Command -> String
cmdNameStr :: Command -> String
cmdNameStr cmd :: Command
cmd = case Command
cmd of
  GlobCmd g :: GlobCmd
g -> GlobCmd -> String
globCmdNameStr GlobCmd
g
  SelectCmd s :: SelectCmd
s _ -> SelectCmd -> String
selectCmdNameStr SelectCmd
s
  TimeLimit _ -> "set time-limit"
  SetAxioms _ -> "set axioms"
  ShowOutput b :: Bool
b -> "show-output " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (Bool -> String
forall a. Show a => a -> String
show Bool
b)
  IncludeProvenTheorems b :: Bool
b -> "set include-theorems " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (Bool -> String
forall a. Show a => a -> String
show Bool
b)
  InspectCmd i :: InspectCmd
i s :: Maybe String
s ->
    (if InspectCmd
i InspectCmd -> InspectCmd -> Bool
forall a. Ord a => a -> a -> Bool
> InspectCmd
Edges then "show-" else "")
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map (\ c :: Char
c -> if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== ' ' then '-' else Char -> Char
toLower Char
c) (InspectCmd -> String
showInspectCmd InspectCmd
i)
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if InspectCmd
i InspectCmd -> InspectCmd -> Bool
forall a. Ord a => a -> a -> Bool
> InspectCmd
LocalAxioms Bool -> Bool -> Bool
&& Maybe String -> Bool
forall a. Maybe a -> Bool
isNothing Maybe String
s Bool -> Bool -> Bool
&& InspectCmd
i InspectCmd -> InspectCmd -> Bool
forall a. Eq a => a -> a -> Bool
/= InspectCmd
ComorphismsTo
        then "-current" else "")
  CommentCmd _ -> "#"
  HelpCmd -> "help"
  ExitCmd -> "quit"
  GroupCmd _ -> ""
  ChangeCmd c :: ChangeCmd
c _ -> ChangeCmd -> String
changeCmdNameStr ChangeCmd
c

-- | show command with arguments
showCmd :: Command -> String
showCmd :: Command -> String
showCmd c :: Command
c = let cn :: String
cn = Command -> String
cmdNameStr Command
c in case Command
c of
  SelectCmd _ t :: String
t -> String
cn String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
t
  TimeLimit l :: Int
l -> String
cn String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l
  SetAxioms as :: [String]
as -> [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
cn String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
as
  CommentCmd s :: String
s -> String
cn String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
  GroupCmd l :: [Command]
l -> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Command -> String) -> [Command] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Command -> String
showCmd [Command]
l
  InspectCmd _ t :: Maybe String
t -> String
cn String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "" Maybe String
t
  ChangeCmd _ t :: String
t -> Command -> String
cmdNameStr Command
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
t
  ShowOutput b :: Bool
b -> String
cn String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. Show a => a -> String
show Bool
b
  _ -> String
cn

describeCmd :: Command -> String
describeCmd :: Command -> String
describeCmd cmd :: Command
cmd = case Command
cmd of
  GlobCmd g :: GlobCmd
g -> GlobCmd -> String
describeGlobCmd GlobCmd
g
  SelectCmd s :: SelectCmd
s _ -> SelectCmd -> String
describeSelectCmd SelectCmd
s
  TimeLimit _ -> "Set the time-limit for the next proof"
  SetAxioms _ -> "Set the axioms used for the next proof"
  ShowOutput b :: Bool
b -> (if Bool
b then "S" else "Do not s")
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ "how model"
  IncludeProvenTheorems b :: Bool
b -> (if Bool
b then "I" else "Do not i")
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ "nclude proven theorems"
  InspectCmd i :: InspectCmd
i t :: Maybe String
t -> if InspectCmd
i InspectCmd -> InspectCmd -> Bool
forall a. Eq a => a -> a -> Bool
== InspectCmd
ComorphismsTo
   then "Show comorphisms from currently selected node(s) to target logic"
   else "Show " String -> ShowS
forall a. [a] -> [a] -> [a]
++ InspectCmd -> String
showInspectCmd InspectCmd
i
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if InspectCmd
i InspectCmd -> InspectCmd -> Bool
forall a. Ord a => a -> a -> Bool
> InspectCmd
LocalAxioms Bool -> Bool -> Bool
&& Maybe String -> Bool
forall a. Maybe a -> Bool
isNothing Maybe String
t then " of selected node" else "")
  CommentCmd _ -> "Line comment"
  HelpCmd -> "Show all available commands"
  ExitCmd -> "Quit"
  GroupCmd _ -> "Grouping several commands"
  ChangeCmd c :: ChangeCmd
c _ -> ChangeCmd -> String
describeChangeCmd ChangeCmd
c

commandList :: [Command]
commandList :: [Command]
commandList =
  (GlobCmd -> Command) -> [GlobCmd] -> [Command]
forall a b. (a -> b) -> [a] -> [b]
map GlobCmd -> Command
GlobCmd [GlobCmd]
globCmdList
  [Command] -> [Command] -> [Command]
forall a. [a] -> [a] -> [a]
++ (SelectCmd -> Command) -> [SelectCmd] -> [Command]
forall a b. (a -> b) -> [a] -> [b]
map SelectCmd -> Command
mkSelectCmd [SelectCmd]
selectCmdList
  [Command] -> [Command] -> [Command]
forall a. [a] -> [a] -> [a]
++ [Int -> Command
TimeLimit 0, [String] -> Command
SetAxioms []]
  [Command] -> [Command] -> [Command]
forall a. [a] -> [a] -> [a]
++ (Bool -> Command) -> [Bool] -> [Command]
forall a b. (a -> b) -> [a] -> [b]
map Bool -> Command
IncludeProvenTheorems [Bool
False, Bool
True]
  [Command] -> [Command] -> [Command]
forall a. [a] -> [a] -> [a]
++ (InspectCmd -> Command) -> [InspectCmd] -> [Command]
forall a b. (a -> b) -> [a] -> [b]
map ((InspectCmd -> Maybe String -> Command)
-> Maybe String -> InspectCmd -> Command
forall a b c. (a -> b -> c) -> b -> a -> c
flip InspectCmd -> Maybe String -> Command
InspectCmd (Maybe String -> InspectCmd -> Command)
-> Maybe String -> InspectCmd -> Command
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just "") [InspectCmd]
inspectCmdList
  [Command] -> [Command] -> [Command]
forall a. [a] -> [a] -> [a]
++ (ChangeCmd -> Command) -> [ChangeCmd] -> [Command]
forall a b. (a -> b) -> [a] -> [b]
map ((ChangeCmd -> String -> Command) -> String -> ChangeCmd -> Command
forall a b c. (a -> b -> c) -> b -> a -> c
flip ChangeCmd -> String -> Command
ChangeCmd "") [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. -}