content: {-# LANGUAGE TypeSynonymInstances #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE FlexibleInstances #-}
  {- |
  Module      :  ./OMDoc/Logic_OMDoc.hs
  Description :  Rudimentary Logic-instances for OMDoc
  Copyright   :  (c) Hendrik Iben, Uni Bremen 2005-2007
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  hiben@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  non-portable
  
  Logic and related instances for OMDoc.
  -}
  module OMDoc.Logic_OMDoc where
  
  import Logic.Logic
  import qualified OMDoc.OMDocInterface as OMDoc
  import OMDoc.ATC_OMDoc ()
  
  import Common.Id
  import Data.Maybe (fromMaybe)
  import qualified Data.Set as Set
  import qualified Data.Map as Map
  import Control.Monad (unless)
  import qualified Control.Monad.Fail as Fail
  
  data OMDoc_PUN = OMDoc_PUN
  
  type OMDoc_Sign = OMDoc.Theory
  
  type OMDoc_Morphism = (OMDoc.Inclusion, OMDoc.Theory, OMDoc.Theory)
  
  instance Show OMDoc_PUN where
    show _ = "OMDoc-PUN"
  
  instance Language OMDoc_PUN where
    description _ = "OMDoc-PUN (possible utter nonsense). Logic to deal with OMDoc."
  
  instance Syntax OMDoc_PUN () OMDoc.Symbol () ()
  
  instance Category OMDoc_Sign OMDoc_Morphism where
    ide s =
      (
          OMDoc.TheoryInclusion
            {
                OMDoc.inclusionFrom = OMDoc.mkSymbolRef (OMDoc.theoryId s)
              , OMDoc.inclusionTo = OMDoc.mkSymbolRef (OMDoc.theoryId s)
              , OMDoc.inclusionMorphism = Nothing
              , OMDoc.inclusionId = Just "identity"
              , OMDoc.inclusionConservativity = OMDoc.CNone
            }
        , s
        , s
      )
    composeMorphisms (m1, s1, _) (m2, _, t2) =
          let
            im1' = OMDoc.inclusionMorphism m1
            im2' = OMDoc.inclusionMorphism m2
            compim =
              case (im1', im2') of
                (Nothing, Nothing) -> Nothing
                (Just _, Nothing) -> im1'
                (Nothing, Just _) -> im2'
                (Just im1, Just im2) ->
                  Just
                      OMDoc.Morphism
                        {
                            OMDoc.morphismId = Just $
                              fromMaybe "Unnamed" (OMDoc.morphismId im1)
                              ++ "_comp_"
                              ++ fromMaybe "Unnamed" (OMDoc.morphismId im2)
                          , OMDoc.morphismHiding =
                              OMDoc.morphismHiding im1 ++
                              OMDoc.morphismHiding im2
                          , OMDoc.morphismBase =
                              OMDoc.morphismBase im1 ++
                              OMDoc.morphismBase im2
                          , OMDoc.morphismRequations =
                              OMDoc.morphismRequations im1 ++
                              OMDoc.morphismRequations im2
                        }
          in
            return (m1 { OMDoc.inclusionMorphism = compim }, s1, t2)
    dom (_, s, _) = s
    cod (_, _, t) = t
    legal_mor (m, s, t) = unless
      (OMDoc.inclusionFrom m == OMDoc.mkSymbolRef (OMDoc.theoryId s)
       &&
       OMDoc.inclusionTo m == OMDoc.mkSymbolRef (OMDoc.theoryId t)) $
      Fail.fail "illegal OMDoc morphism"
  
  instance Sentences OMDoc_PUN () OMDoc_Sign OMDoc_Morphism OMDoc.Symbol where
    sym_of OMDoc_PUN s =
        singletonList
        $ Set.fromList $ foldr (\ sy -> case sy of
                            OMDoc.CSy s' -> (s' :)
                            _ -> id) []
              $ OMDoc.theoryConstitutives s
    symmap_of OMDoc_PUN (m, s1, s2) =
      case OMDoc.inclusionMorphism m of
        Nothing -> Map.empty
        (Just im) ->
          foldl
            (\ smap r ->
              case r of
                (OMDoc.MTextOM omobj1, OMDoc.MTextOM omobj2) ->
                  case (omobj1, omobj2) of
                    (OMDoc.OMObject (OMDoc.OMES oms1), OMDoc.OMObject (OMDoc.OMES oms2)) ->
                      let
                        name1 = OMDoc.omsName oms1
                        name2 = OMDoc.omsName oms2
                        msymbol1 =
                          case
                            filter
                              (\ c ->
                                case c of
                                  (OMDoc.CSy symbol) ->
                                    OMDoc.symbolId symbol == name1
                                  _ ->
                                    False
                              )
                              (OMDoc.theoryConstitutives s1)
                          of
                            [] -> Nothing
                            (OMDoc.CSy symbol : _) -> Just symbol
                            _ -> error "OMDoc.Logic_OMDoc.symmap_of"
                        msymbol2 =
                          case
                            filter
                              (\ c ->
                                case c of
                                  (OMDoc.CSy symbol) ->
                                    OMDoc.symbolId symbol == name2
                                  _ ->
                                    False
                              )
                              (OMDoc.theoryConstitutives s2)
                          of
                            [] -> Nothing
                            (OMDoc.CSy symbol : _) -> Just symbol
                            _ -> error "OMDoc.Logic_OMDoc.symmap_of"
                        newmap =
                          case (msymbol1, msymbol2) of
                            (Nothing, _) -> smap
                            (_, Nothing) -> smap
                            (Just symbol1, Just symbol2) ->
                              Map.insert symbol1 symbol2 smap
                      in
                        newmap
                    _ -> smap
                _ ->
                  smap
            )
            Map.empty
            (OMDoc.morphismRequations im)
    sym_name OMDoc_PUN s =
      -- real Id's are saved as Presentation-Elements...
      stringToId $ OMDoc.symbolId s
    symKind OMDoc_PUN = show . OMDoc.symbolRole
  
  instance StaticAnalysis OMDoc_PUN () () () () OMDoc_Sign OMDoc_Morphism OMDoc.Symbol () where
    symbol_to_raw OMDoc_PUN _ = ()
    id_to_raw OMDoc_PUN _ = ()
    matches OMDoc_PUN _ _ = False
    empty_signature OMDoc_PUN =
      OMDoc.Theory
      {
          OMDoc.theoryId = "empty"
        , OMDoc.theoryConstitutives = []
        , OMDoc.theoryPresentations = []
        , OMDoc.theoryComment = Nothing
      }
  
  is_subsig :: OMDoc.Theory -> OMDoc.Theory -> Bool
  is_subsig s1 s2 =
      -- This currently only checks symbols. Maybe ADTs should also be checked...
      let
        s1sym =
          foldl
            (\ s con ->
              case con of
                (OMDoc.CSy sym) ->
                  Set.insert sym s
                _ ->
                  s
            )
            Set.empty
            (OMDoc.theoryConstitutives s1)
        s2sym =
          foldl
            (\ s con ->
              case con of
                (OMDoc.CSy sym) ->
                  Set.insert sym s
                _ ->
                  s
            )
            Set.empty
            (OMDoc.theoryConstitutives s2)
      in
       Set.isSubsetOf s1sym s2sym
  
  instance Logic OMDoc_PUN () () () () () OMDoc_Sign OMDoc_Morphism OMDoc.Symbol () ()
  