55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maeder{- |

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis TsogiasModule : $Header$

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : development graph commands for all interfaces

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis TsogiasCopyright : (c) Christian Maeder, DFKI GmbH 2009

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis TsogiasLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis TsogiasMaintainer : Christian.Maeder@dfki.de

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis TsogiasStability : provisional

ad1df93673cf323534cdfe18981ad5daae4c90c0Jonathan von SchroederPortability : portable

1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogiasdata types for development graph commands to be invoked via the GUI, the

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogiascommand-line-interface (CMDL), and other tools

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias-}

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogiasmodule Interfaces.Command where

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogiasimport Common.Utils

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogiasimport Data.Char

f88f637f3c7ff472142b07dcc12230375a5f1c28Christian Maederimport Data.List

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogiasdata GlobCmd =

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder Automatic

87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder | GlobDecomp

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder | GlobSubsume

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder | LocalDecomp

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder | LocalInference

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias | CompositionProveEdges

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias | CompositionCreateEdges

87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder | Conservativity

4e95ffc23b9c5f0b5980ab6f1cacbe7bd9789851Alexis Tsogias | ThmHideShift

4e95ffc23b9c5f0b5980ab6f1cacbe7bd9789851Alexis Tsogias | HideThmShift

421def3c7b0b9ca7762f809a2c57c6ee74495ffaJonathan von Schroeder | Colimit

4b9f1c9f95296f3292b2e53dbc3d196751b862dbJonathan von Schroeder | NormalForm

7dc37844730a8b23973139e9720574382de109e7Alexis Tsogias | Freeness

93c8c4a8ce75cc2e02e03468a97b896f149d26ceAlexis Tsogias | QualifyNames

9d05f30775dd499da9e262b5c199b63c86cc239bJonathan von Schroeder | UndoCmd

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder | RedoCmd

91673dab8e4e249ffb3efe5edab8351dfaf4977dJonathan von Schroeder -- Flattening command

91673dab8e4e249ffb3efe5edab8351dfaf4977dJonathan von Schroeder | Importing

9503f59b8e16c517ba75df2512b80b354759ad1aJonathan von Schroeder | DisjointUnion

9503f59b8e16c517ba75df2512b80b354759ad1aJonathan von Schroeder | Renaming

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias | Hiding

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder | Heterogeneity

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis Tsogias | ProveCurrent -- CMDL prover activation

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias | DropTranslation -- stop composing comorphisms to previous ones

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias deriving (Eq, Ord, Enum, Bounded)

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis TsogiasglobCmdList :: [GlobCmd]

beb399aad2f2d329dea36508625352fddee3c302Christian MaederglobCmdList = [minBound .. maxBound]

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis Tsogias

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis Tsogias-- list of command names in the gui interface

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis TsogiasmenuTextGlobCmd :: GlobCmd -> String

e16b3696b2c173aac14200321868ed81b8f7dc69Christian MaedermenuTextGlobCmd cmd = case cmd of

9d05f30775dd499da9e262b5c199b63c86cc239bJonathan von Schroeder Automatic -> "Automatic"

9d05f30775dd499da9e262b5c199b63c86cc239bJonathan von Schroeder GlobDecomp -> "Global-Decomposition"

9d05f30775dd499da9e262b5c199b63c86cc239bJonathan von Schroeder GlobSubsume -> "Global-Subsumption"

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder LocalDecomp -> "Local-Decomposition"

a65c6747c9acbbebc93baba7bae94d2e3d8cdafbTill Mossakowski LocalInference -> "Local-Inference"

87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder CompositionProveEdges -> "Prove composed edges"

1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias CompositionCreateEdges -> "Create composed proven edges"

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias Conservativity -> "Conservativity"

8394b397aadaf0c2bfc19c0628f17f83f031a759Jonathan von Schroeder ThmHideShift -> "Theorem-Hide-Shift"

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias HideThmShift -> "Hide-Theorem-Shift"

8394b397aadaf0c2bfc19c0628f17f83f031a759Jonathan von Schroeder Colimit -> "Compute colimit"

91673dab8e4e249ffb3efe5edab8351dfaf4977dJonathan von Schroeder NormalForm -> "Compute normal form"

91673dab8e4e249ffb3efe5edab8351dfaf4977dJonathan von Schroeder QualifyNames -> "Qualify all names"

91673dab8e4e249ffb3efe5edab8351dfaf4977dJonathan von Schroeder UndoCmd -> "Undo"

91673dab8e4e249ffb3efe5edab8351dfaf4977dJonathan von Schroeder RedoCmd -> "Redo"

91673dab8e4e249ffb3efe5edab8351dfaf4977dJonathan von Schroeder Importing -> "Importing"

9503f59b8e16c517ba75df2512b80b354759ad1aJonathan von Schroeder DisjointUnion -> "Disjoint union"

91673dab8e4e249ffb3efe5edab8351dfaf4977dJonathan von Schroeder Renaming -> "Renaming"

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder Hiding -> "Hiding"

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias Freeness -> "Freeness"

8394b397aadaf0c2bfc19c0628f17f83f031a759Jonathan von Schroeder Heterogeneity -> "Heterogeneity"

1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias ProveCurrent -> "Prove"

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis Tsogias DropTranslation -> "Drop-Translations"

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis Tsogias

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis Tsogias-- | even some short names for the command line interface

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis TsogiascmdlGlobCmd :: GlobCmd -> String

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis TsogiascmdlGlobCmd cmd = case cmd of

1566df29333319b713031b86c7d18171e5a009bdJonathan von Schroeder Automatic -> "auto"

1566df29333319b713031b86c7d18171e5a009bdJonathan von Schroeder GlobDecomp -> "glob-decomp"

f88f637f3c7ff472142b07dcc12230375a5f1c28Christian Maeder GlobSubsume -> "global-subsume"

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias LocalDecomp -> "loc-decomp"

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder LocalInference -> "local-infer"

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder CompositionProveEdges -> "comp"

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder CompositionCreateEdges -> "comp-new"

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder Conservativity -> "cons"

8394b397aadaf0c2bfc19c0628f17f83f031a759Jonathan von Schroeder ThmHideShift -> "thm-hide"

1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias HideThmShift -> "hide-thm"

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder _ -> map toLower $ menuTextGlobCmd cmd

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis Tsogias

e24ad3f655daa60ddabe690e4b11de3187996c16cmaederisDgRule :: GlobCmd -> Bool

e24ad3f655daa60ddabe690e4b11de3187996c16cmaederisDgRule c = c <= HideThmShift

e24ad3f655daa60ddabe690e4b11de3187996c16cmaeder

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von SchroederisFlatteningCmd :: GlobCmd -> Bool

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von SchroederisFlatteningCmd c = c >= Importing && c <= Heterogeneity

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von SchroederisUndoOrRedo :: GlobCmd -> Bool

8c7aa750542dcadb94b971be712564a9a8f1d189Christian MaederisUndoOrRedo c = elem c [UndoCmd, RedoCmd]

55dfa79a16e5f0ddb60bceab3717c07e62e65846Jonathan von Schroeder

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von SchroederdescribeGlobCmd :: GlobCmd -> String

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von SchroederdescribeGlobCmd c =

8c7aa750542dcadb94b971be712564a9a8f1d189Christian Maeder let mt = menuTextGlobCmd c

87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder t = map toLower mt in

8c030738bc90ffb417074a9502c0bac2ed414e2eJonathan von Schroeder case c of

55dfa79a16e5f0ddb60bceab3717c07e62e65846Jonathan von Schroeder Automatic -> "Apply automatic tactic"

87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder CompositionProveEdges -> t

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder CompositionCreateEdges -> t

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder QualifyNames -> "Qualify and disambiguate all signature names"

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder NormalForm -> "Compute normal forms for nodes with incoming hiding links"

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder Importing -> "Flatten all theories and delete all importing links"

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder DisjointUnion -> "Create intersection nodes and ensure only disjoint unions"

87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder Hiding -> "Delete all hiding links"

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder ProveCurrent -> "Applies selected prover to selected goals"

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder DropTranslation -> "Drops any selected comorphism"

55dfa79a16e5f0ddb60bceab3717c07e62e65846Jonathan von Schroeder _ -> if isDgRule c then "Apply rule " ++ t else

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder if isFlatteningCmd c then "Flatten out " ++ t else

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder if isUndoOrRedo c then mt ++ " last change" else t

8c7aa750542dcadb94b971be712564a9a8f1d189Christian Maeder

8c7aa750542dcadb94b971be712564a9a8f1d189Christian MaederglobCmdNameStr :: GlobCmd -> String

55dfa79a16e5f0ddb60bceab3717c07e62e65846Jonathan von SchroederglobCmdNameStr c = let s = cmdlGlobCmd c in

0f1637f1e645957ce9e29926d3d2607ea8498961Jonathan von Schroeder if isDgRule c then "dg-all " ++ s else

8c7aa750542dcadb94b971be712564a9a8f1d189Christian Maeder if isFlatteningCmd c then "flattening " ++ s else s

55dfa79a16e5f0ddb60bceab3717c07e62e65846Jonathan von Schroeder

0f1637f1e645957ce9e29926d3d2607ea8498961Jonathan von Schroeder-- | select a named entity

0f1637f1e645957ce9e29926d3d2607ea8498961Jonathan von Schroederdata SelectCmd =

8c7aa750542dcadb94b971be712564a9a8f1d189Christian Maeder LibFile -- read library from file

55dfa79a16e5f0ddb60bceab3717c07e62e65846Jonathan von Schroeder | Lib -- allows to move to an imported library

55dfa79a16e5f0ddb60bceab3717c07e62e65846Jonathan von Schroeder | Node

55dfa79a16e5f0ddb60bceab3717c07e62e65846Jonathan von Schroeder | ComorphismTranslation

8c7aa750542dcadb94b971be712564a9a8f1d189Christian Maeder | Prover

55dfa79a16e5f0ddb60bceab3717c07e62e65846Jonathan von Schroeder | Goal -- a single goal for an automatic prover

55dfa79a16e5f0ddb60bceab3717c07e62e65846Jonathan von Schroeder | ConsistencyChecker

bf453a6867cca0aa530bc8cac9eed9c3f70594b4Jonathan von Schroeder | Link

0f1637f1e645957ce9e29926d3d2607ea8498961Jonathan von Schroeder | ConservativityChecker

0f1637f1e645957ce9e29926d3d2607ea8498961Jonathan von Schroeder deriving (Enum, Bounded)

0f1637f1e645957ce9e29926d3d2607ea8498961Jonathan von Schroeder

55dfa79a16e5f0ddb60bceab3717c07e62e65846Jonathan von SchroederselectCmdList :: [SelectCmd]

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von SchroederselectCmdList = [minBound .. maxBound]

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder

8c7aa750542dcadb94b971be712564a9a8f1d189Christian MaederselectCmdNameStr :: SelectCmd -> String

9d05f30775dd499da9e262b5c199b63c86cc239bJonathan von SchroederselectCmdNameStr cmd = case cmd of

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder LibFile -> "use"

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder Lib -> "library"

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder Node -> "dg basic"

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder ComorphismTranslation -> "translate"

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder Prover -> "prover"

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder Goal -> "set goals"

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder ConsistencyChecker -> "cons-checker"

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder Link -> "link"

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder ConservativityChecker -> "conservativity-check"

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von SchroederdescribeSelectCmd :: SelectCmd -> String

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von SchroederdescribeSelectCmd cmd = case cmd of

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder LibFile -> "Read HetCASL file"

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder Lib -> "Select library"

3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder Node -> "Select node"

ComorphismTranslation -> "Choose translation"

Prover -> "Choose prover"

Goal -> "Set goal"

ConsistencyChecker -> "Choose consistency checker"

Link -> "Select link"

ConservativityChecker -> "Choose conservativity checker"

data InspectCmd =

CmdList -- all possible commands

| Libs -- all imported libraries

| Nodes -- of library

| Edges

| UndoHist

| RedoHist

| NodeInfo -- of a selected node

| Theory

| AllGoals

| ProvenGoals

| UnprovenGoals

| Axioms

| LocalAxioms

| Taxonomy

| Concept

| EdgeInfo -- of a selected link

deriving (Eq, Ord, Enum, Bounded)

inspectCmdList :: [InspectCmd]

inspectCmdList = [minBound .. maxBound]

showInspectCmd :: InspectCmd -> String

showInspectCmd cmd = case cmd of

CmdList -> "Details" -- all possible commands

Libs -> "Library Names"

Nodes -> "Nodes"

Edges -> "Edges"

UndoHist -> "Undo-History"

RedoHist -> "Redo-History"

NodeInfo -> "Node-Info"

Theory -> "Computed Theory"

AllGoals -> "All Goals"

ProvenGoals -> "Proven Goals"

UnprovenGoals -> "Unproven Goals"

Axioms -> "All Axioms"

LocalAxioms -> "Local Axioms"

Taxonomy -> "Taxonomy"

Concept -> "Concept"

EdgeInfo -> "Edge-Info"

requiresNode :: InspectCmd -> Bool

requiresNode ic = ic >= NodeInfo && ic < EdgeInfo

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

| IncludeProvenTheorems Bool -- should proven theorems be added as axioms

| InspectCmd InspectCmd

| CommentCmd String

| GroupCmd [Command] -- just to group commands in addCommandHistoryToState

mkSelectCmd :: SelectCmd -> Command

mkSelectCmd s = SelectCmd s ""

cmdInputStr :: Command -> String

cmdInputStr cmd = case cmd of

SelectCmd _ t -> t

TimeLimit l -> show l

SetAxioms as -> unwords as

_ -> ""

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

_ -> cmd

cmdNameStr :: Command -> String

cmdNameStr cmd = case cmd of

GlobCmd g -> globCmdNameStr g

SelectCmd s _ -> selectCmdNameStr s

TimeLimit _ -> "set time-limit"

SetAxioms _ -> "set axioms"

IncludeProvenTheorems b -> "set include-theorems " ++ map toLower (show b)

InspectCmd i -> (if i > Edges then "show-" else "")

++ map (\ c -> if c == ' ' then '-' else toLower c) (showInspectCmd i)

CommentCmd _ -> "#"

GroupCmd _ -> ""

-- | show command with arguments

showCmd :: Command -> String

showCmd c = case c of

SelectCmd _ t -> cmdNameStr c ++ " " ++ t

TimeLimit l -> cmdNameStr c ++ " " ++ show l

SetAxioms as -> unwords $ cmdNameStr c : as

CommentCmd s -> cmdNameStr c ++ s

GroupCmd l -> intercalate "\n" $ map showCmd l

_ -> cmdNameStr c

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"

IncludeProvenTheorems b -> (if b then "I" else "Do not i")

++ "nclude proven theorems"

InspectCmd i -> "Show " ++ showInspectCmd i

CommentCmd _ -> "Line comment"

GroupCmd _ -> "Grouping several commands"

commandList :: [Command]

commandList =

map GlobCmd globCmdList

++ map (\ s -> SelectCmd s "") selectCmdList

++ [TimeLimit 0, SetAxioms []]

++ map IncludeProvenTheorems [False, True]

++ map InspectCmd inspectCmdList

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