{- |
Module      :  ./Interfaces/CmdAction.hs
Description :  command action associations 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

association of some commands to actions on development graphs
-}

module Interfaces.CmdAction where

import Proofs.QualifyNames (qualifyLibEnv)
import Proofs.DGFlattening
import Proofs.Freeness (freeness)
import Proofs.NormalForm (normalForm)
import Proofs.Automatic (automatic)
import Proofs.Global (globSubsume, globDecomp)
import Proofs.Local (localInference, locDecomp)
import Proofs.Composition (composition, compositionCreatingEdges)
import Proofs.HideTheoremShift (automaticHideTheoremShift)
import Proofs.TheoremHideShift (theoremHideShift)
import Proofs.Conservativity (conservativity)
import Proofs.ComputeColimit (computeColimit)
import Proofs.TriangleCons (triangleCons)

import Static.DevGraph

import Interfaces.Command

import Common.LibName
import Common.Result

globLibAct :: [(GlobCmd, LibName -> LibEnv -> LibEnv)]
globLibAct :: [(GlobCmd, LibName -> LibEnv -> LibEnv)]
globLibAct =
  [ (GlobCmd
Automatic, LibName -> LibEnv -> LibEnv
automatic)
  , (GlobCmd
GlobDecomp, LibName -> LibEnv -> LibEnv
globDecomp)
  , (GlobCmd
GlobSubsume, LibName -> LibEnv -> LibEnv
globSubsume)
  , (GlobCmd
LocalDecomp, LibName -> LibEnv -> LibEnv
locDecomp)
  , (GlobCmd
LocalInference, LibName -> LibEnv -> LibEnv
localInference)
  , (GlobCmd
CompositionProveEdges, LibName -> LibEnv -> LibEnv
composition)
  , (GlobCmd
CompositionCreateEdges, LibName -> LibEnv -> LibEnv
compositionCreatingEdges)
  , (GlobCmd
Conservativity, LibName -> LibEnv -> LibEnv
conservativity)
  , (GlobCmd
HideThmShift, LibName -> LibEnv -> LibEnv
automaticHideTheoremShift) ]

globLibResultAct :: [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
globLibResultAct :: [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
globLibResultAct =
  [ (GlobCmd
ThmHideShift, LibName -> LibEnv -> Result LibEnv
theoremHideShift)
  , (GlobCmd
Colimit, LibName -> LibEnv -> Result LibEnv
computeColimit)
  , (GlobCmd
NormalForm, LibName -> LibEnv -> Result LibEnv
normalForm)
  , (GlobCmd
TriangleCons, LibName -> LibEnv -> Result LibEnv
triangleCons)
  , (GlobCmd
Freeness, LibName -> LibEnv -> Result LibEnv
freeness)
-- , (ThmFreeShift, theoremFreeShift)
  ]

allGlobLibAct :: [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
allGlobLibAct :: [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
allGlobLibAct =
  ((GlobCmd, LibName -> LibEnv -> LibEnv)
 -> (GlobCmd, LibName -> LibEnv -> Result LibEnv))
-> [(GlobCmd, LibName -> LibEnv -> LibEnv)]
-> [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: GlobCmd
a, b :: LibName -> LibEnv -> LibEnv
b) -> (GlobCmd
a, \ n :: LibName
n -> LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> Result LibEnv)
-> (LibEnv -> LibEnv) -> LibEnv -> Result LibEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibName -> LibEnv -> LibEnv
b LibName
n)) [(GlobCmd, LibName -> LibEnv -> LibEnv)]
globLibAct
  [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
-> [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
-> [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
forall a. [a] -> [a] -> [a]
++ [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
globLibResultAct
  [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
-> [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
-> [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
forall a. [a] -> [a] -> [a]
++ ((GlobCmd, LibEnv -> Result LibEnv)
 -> (GlobCmd, LibName -> LibEnv -> Result LibEnv))
-> [(GlobCmd, LibEnv -> Result LibEnv)]
-> [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: GlobCmd
a, b :: LibEnv -> Result LibEnv
b) -> (GlobCmd
a, (LibEnv -> Result LibEnv) -> LibName -> LibEnv -> Result LibEnv
forall a b. a -> b -> a
const LibEnv -> Result LibEnv
b)) [(GlobCmd, LibEnv -> Result LibEnv)]
globResultAct

globResultAct :: [(GlobCmd, LibEnv -> Result LibEnv)]
globResultAct :: [(GlobCmd, LibEnv -> Result LibEnv)]
globResultAct =
  [ (GlobCmd
Importing, LibEnv -> Result LibEnv
libFlatImports)
  , (GlobCmd
DisjointUnion, LibEnv -> Result LibEnv
libFlatDUnions)
  , (GlobCmd
Renaming, LibEnv -> Result LibEnv
libFlatRenamings)
  , (GlobCmd
Hiding, LibEnv -> Result LibEnv
libFlatHiding)
  , (GlobCmd
Heterogeneity, LibEnv -> Result LibEnv
libFlatHeterogen)
  , (GlobCmd
QualifyNames, LibEnv -> Result LibEnv
qualifyLibEnv) ]