{- |
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 =
[ (Automatic, automatic)
, (GlobDecomp, globDecomp)
, (GlobSubsume, globSubsume)
, (LocalDecomp, locDecomp)
, (LocalInference, localInference)
, (CompositionProveEdges, composition)
, (CompositionCreateEdges, compositionCreatingEdges)
, (Conservativity, conservativity)
, (HideThmShift, automaticHideTheoremShift) ]
globLibResultAct :: [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
globLibResultAct =
[ (ThmHideShift, theoremHideShift)
, (Colimit, computeColimit)
, (NormalForm, normalForm)
, (TriangleCons, triangleCons)
, (Freeness, freeness)
-- , (ThmFreeShift, theoremFreeShift)
]
allGlobLibAct :: [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
allGlobLibAct =
map (\ (a, b) -> (a, \ n -> return . b n)) globLibAct
++ globLibResultAct
++ map (\ (a, b) -> (a, const b)) globResultAct
globResultAct :: [(GlobCmd, LibEnv -> Result LibEnv)]
globResultAct =
[ (Importing, libFlatImports)
, (DisjointUnion, libFlatDUnions)
, (Renaming, libFlatRenamings)
, (Hiding, libFlatHiding)
, (Heterogeneity, libFlatHeterogen)
, (QualifyNames, qualifyLibEnv) ]