content: {- |
  Module      :  ./Static/SpecLoader.hs
  Description :  For loading of signatures and sentences from file
  Copyright   :  (c)  C. Maeder, DFKI GmbH 2010
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Ewaryst.Schulz@dfki.de
  Stability   :  experimental
  Portability :  non-portable (import Logic)
  
  For loading of signatures and sentences from file
  -}
  
  module Static.SpecLoader where
  
  import Static.AnalysisLibrary
  import Static.GTheory
  import Static.DevGraph
  import Static.ComputeTheory
  
  import Driver.Options
  
  import qualified Common.OrderedMap as OMap
  import Common.GlobalAnnotations
  import Common.AS_Annotation as Anno
  import Common.Result
  import Common.ResultT
  import Common.LibName
  import Common.Id as Id
  import Common.IRI (simpleIdToIRI)
  import Common.ExtSign
  
  import Data.Graph.Inductive.Graph
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  
  -- Logic things
  import Logic.Coerce
  import Logic.Logic
  import Comorphisms.LogicGraph
  
  
  proceed' :: HetcatsOpts -> FilePath -> ResultT IO (LibName, LibEnv)
  proceed' hopts = anaSourceFile logicGraph hopts Set.empty emptyLibEnv emptyDG
  
  data SigSens sign sentence =
      SigSens
      { sigsensSignature :: sign
      , sigsensNamedSentences :: [Named sentence]
      , sigsensGlobalAnnos :: GlobalAnnos
      , sigsensNode :: Node
      , sigsensNodeLabel :: DGNodeLab
      , sigsensDG :: DGraph
      , sigsensLibname :: LibName
      , sigsensLibenv :: LibEnv }
  
  getSigSensComplete ::
      Logic lid sublogics basic_spec sentence
            symb_items symb_map_items sign
            morphism symbol raw_symbol proof_tree
      => Bool -- complete theory or not
      -> HetcatsOpts -- options
      -> lid -- logicname
      -> String -- filename
      -> String  -- name of spec
      -> IO (SigSens sign sentence)
  getSigSensComplete b hopts lid fname sp = do
    Result _ res <- runResultT $ proceed' hopts fname
    case res of
      Just (ln, lenv) -> getSpec b lid ln lenv sp
      Nothing -> error $ "getSigSensComplete: cannot read file" ++ fname
  
  
  -- read in a hets file and return the basic theory and the sentences
  getSigSens ::
      Logic lid sublogics basic_spec sentence
            symb_items symb_map_items sign
            morphism symbol raw_symbol proof_tree
      => HetcatsOpts -- options
      -> lid -- logicname
      -> String -- filename
      -> String  -- name of spec
      -> IO (SigSens sign sentence)
  getSigSens = getSigSensComplete False
  
  
  getSpec ::
      Logic lid sublogics basic_spec sentence
            symb_items symb_map_items sign
            morphism symbol raw_symbol proof_tree
      => Bool -- complete theory or not
      -> lid -- logicname
      -> LibName
      -> LibEnv
      -> String  -- name of spec
      -> IO (SigSens sign sentence)
  getSpec b lid ln lenv sp =
      let dg = lookupDGraph ln lenv
          SpecEntry (ExtGenSig _ (NodeSig node _)) =
              case Map.lookup (simpleIdToIRI $ Id.mkSimpleId sp) $ globalEnv dg of
                Just x -> x
                _ -> error $ "getSpec: Specification " ++ sp ++ " not found"
          f nL gth =
              case gth of
                G_theory { gTheoryLogic = lid2
                         , gTheorySign = gSig
                         , gTheorySens = gSens } ->
                       case (coerceSign lid2 lid "" gSig,
                             coerceThSens lid2 lid "" gSens) of
                         (Just sig, Just sens) ->
                             return SigSens
                                        { sigsensSignature = plainSign sig
                                        , sigsensNamedSentences
                                            = map (\ (x, y) -> y {senAttr = x})
                                              $ OMap.toList sens
                                        , sigsensGlobalAnnos = globalAnnos dg
                                        , sigsensNode = node
                                        , sigsensNodeLabel = nL
                                        , sigsensDG = dg
                                        , sigsensLibname = ln
                                        , sigsensLibenv = lenv }
                         _ -> error $ "getSpec: Not a " ++ show lid ++ " sig"
  
      in if b then
             case computeTheory lenv ln node of
               Just gth -> f (labDG dg node) gth
               _ -> error "getSpec: computeTheory failed"
         else
             case match node (dgBody dg) of
               (Just ctx, _) ->
                   let nL = lab' ctx in f nL $ dgn_theory nL
               _ -> error $ "getSpec: Node " ++ show node
                    ++ " not in development graph"
  