{- |
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) ]
