{-# 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 -> String
show _ = "OMDoc-PUN"

instance Language OMDoc_PUN where
  description :: OMDoc_PUN -> String
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 :: OMDoc_Sign -> OMDoc_Morphism
ide s :: OMDoc_Sign
s =
    (
        TheoryInclusion :: OMDocRef
-> OMDocRef
-> Maybe Morphism
-> Maybe String
-> Conservativity
-> Inclusion
OMDoc.TheoryInclusion
          {
              inclusionFrom :: OMDocRef
OMDoc.inclusionFrom = String -> OMDocRef
OMDoc.mkSymbolRef (OMDoc_Sign -> String
OMDoc.theoryId OMDoc_Sign
s)
            , inclusionTo :: OMDocRef
OMDoc.inclusionTo = String -> OMDocRef
OMDoc.mkSymbolRef (OMDoc_Sign -> String
OMDoc.theoryId OMDoc_Sign
s)
            , inclusionMorphism :: Maybe Morphism
OMDoc.inclusionMorphism = Maybe Morphism
forall a. Maybe a
Nothing
            , inclusionId :: Maybe String
OMDoc.inclusionId = String -> Maybe String
forall a. a -> Maybe a
Just "identity"
            , inclusionConservativity :: Conservativity
OMDoc.inclusionConservativity = Conservativity
OMDoc.CNone
          }
      , OMDoc_Sign
s
      , OMDoc_Sign
s
    )
  composeMorphisms :: OMDoc_Morphism -> OMDoc_Morphism -> Result OMDoc_Morphism
composeMorphisms (m1 :: Inclusion
m1, s1 :: OMDoc_Sign
s1, _) (m2 :: Inclusion
m2, _, t2 :: OMDoc_Sign
t2) =
        let
          im1' :: Maybe Morphism
im1' = Inclusion -> Maybe Morphism
OMDoc.inclusionMorphism Inclusion
m1
          im2' :: Maybe Morphism
im2' = Inclusion -> Maybe Morphism
OMDoc.inclusionMorphism Inclusion
m2
          compim :: Maybe Morphism
compim =
            case (Maybe Morphism
im1', Maybe Morphism
im2') of
              (Nothing, Nothing) -> Maybe Morphism
forall a. Maybe a
Nothing
              (Just _, Nothing) -> Maybe Morphism
im1'
              (Nothing, Just _) -> Maybe Morphism
im2'
              (Just im1 :: Morphism
im1, Just im2 :: Morphism
im2) ->
                Morphism -> Maybe Morphism
forall a. a -> Maybe a
Just
                    Morphism :: Maybe String
-> [String] -> [String] -> [(MText, MText)] -> Morphism
OMDoc.Morphism
                      {
                          morphismId :: Maybe String
OMDoc.morphismId = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$
                            String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "Unnamed" (Morphism -> Maybe String
OMDoc.morphismId Morphism
im1)
                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_comp_"
                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "Unnamed" (Morphism -> Maybe String
OMDoc.morphismId Morphism
im2)
                        , morphismHiding :: [String]
OMDoc.morphismHiding =
                            Morphism -> [String]
OMDoc.morphismHiding Morphism
im1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                            Morphism -> [String]
OMDoc.morphismHiding Morphism
im2
                        , morphismBase :: [String]
OMDoc.morphismBase =
                            Morphism -> [String]
OMDoc.morphismBase Morphism
im1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                            Morphism -> [String]
OMDoc.morphismBase Morphism
im2
                        , morphismRequations :: [(MText, MText)]
OMDoc.morphismRequations =
                            Morphism -> [(MText, MText)]
OMDoc.morphismRequations Morphism
im1 [(MText, MText)] -> [(MText, MText)] -> [(MText, MText)]
forall a. [a] -> [a] -> [a]
++
                            Morphism -> [(MText, MText)]
OMDoc.morphismRequations Morphism
im2
                      }
        in
          OMDoc_Morphism -> Result OMDoc_Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Inclusion
m1 { inclusionMorphism :: Maybe Morphism
OMDoc.inclusionMorphism = Maybe Morphism
compim }, OMDoc_Sign
s1, OMDoc_Sign
t2)
  dom :: OMDoc_Morphism -> OMDoc_Sign
dom (_, s :: OMDoc_Sign
s, _) = OMDoc_Sign
s
  cod :: OMDoc_Morphism -> OMDoc_Sign
cod (_, _, t :: OMDoc_Sign
t) = OMDoc_Sign
t
  legal_mor :: OMDoc_Morphism -> Result ()
legal_mor (m :: Inclusion
m, s :: OMDoc_Sign
s, t :: OMDoc_Sign
t) = Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
    (Inclusion -> OMDocRef
OMDoc.inclusionFrom Inclusion
m OMDocRef -> OMDocRef -> Bool
forall a. Eq a => a -> a -> Bool
== String -> OMDocRef
OMDoc.mkSymbolRef (OMDoc_Sign -> String
OMDoc.theoryId OMDoc_Sign
s)
     Bool -> Bool -> Bool
&&
     Inclusion -> OMDocRef
OMDoc.inclusionTo Inclusion
m OMDocRef -> OMDocRef -> Bool
forall a. Eq a => a -> a -> Bool
== String -> OMDocRef
OMDoc.mkSymbolRef (OMDoc_Sign -> String
OMDoc.theoryId OMDoc_Sign
t)) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$
    String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "illegal OMDoc morphism"

instance Sentences OMDoc_PUN () OMDoc_Sign OMDoc_Morphism OMDoc.Symbol where
  sym_of :: OMDoc_PUN -> OMDoc_Sign -> [Set Symbol]
sym_of OMDoc_PUN s :: OMDoc_Sign
s =
      Set Symbol -> [Set Symbol]
forall a. a -> [a]
singletonList
      (Set Symbol -> [Set Symbol]) -> Set Symbol -> [Set Symbol]
forall a b. (a -> b) -> a -> b
$ [Symbol] -> Set Symbol
forall a. Ord a => [a] -> Set a
Set.fromList ([Symbol] -> Set Symbol) -> [Symbol] -> Set Symbol
forall a b. (a -> b) -> a -> b
$ (Constitutive -> [Symbol] -> [Symbol])
-> [Symbol] -> [Constitutive] -> [Symbol]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ sy :: Constitutive
sy -> case Constitutive
sy of
                          OMDoc.CSy s' :: Symbol
s' -> (Symbol
s' Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:)
                          _ -> [Symbol] -> [Symbol]
forall a. a -> a
id) []
            ([Constitutive] -> [Symbol]) -> [Constitutive] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ OMDoc_Sign -> [Constitutive]
OMDoc.theoryConstitutives OMDoc_Sign
s
  symmap_of :: OMDoc_PUN -> OMDoc_Morphism -> EndoMap Symbol
symmap_of OMDoc_PUN (m :: Inclusion
m, s1 :: OMDoc_Sign
s1, s2 :: OMDoc_Sign
s2) =
    case Inclusion -> Maybe Morphism
OMDoc.inclusionMorphism Inclusion
m of
      Nothing -> EndoMap Symbol
forall k a. Map k a
Map.empty
      (Just im :: Morphism
im) ->
        (EndoMap Symbol -> (MText, MText) -> EndoMap Symbol)
-> EndoMap Symbol -> [(MText, MText)] -> EndoMap Symbol
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
          (\ smap :: EndoMap Symbol
smap r :: (MText, MText)
r ->
            case (MText, MText)
r of
              (OMDoc.MTextOM omobj1 :: OMObject
omobj1, OMDoc.MTextOM omobj2 :: OMObject
omobj2) ->
                case (OMObject
omobj1, OMObject
omobj2) of
                  (OMDoc.OMObject (OMDoc.OMES oms1 :: OMSymbol
oms1), OMDoc.OMObject (OMDoc.OMES oms2 :: OMSymbol
oms2)) ->
                    let
                      name1 :: String
name1 = OMSymbol -> String
OMDoc.omsName OMSymbol
oms1
                      name2 :: String
name2 = OMSymbol -> String
OMDoc.omsName OMSymbol
oms2
                      msymbol1 :: Maybe Symbol
msymbol1 =
                        case
                          (Constitutive -> Bool) -> [Constitutive] -> [Constitutive]
forall a. (a -> Bool) -> [a] -> [a]
filter
                            (\ c :: Constitutive
c ->
                              case Constitutive
c of
                                (OMDoc.CSy symbol :: Symbol
symbol) ->
                                  Symbol -> String
OMDoc.symbolId Symbol
symbol String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
name1
                                _ ->
                                  Bool
False
                            )
                            (OMDoc_Sign -> [Constitutive]
OMDoc.theoryConstitutives OMDoc_Sign
s1)
                        of
                          [] -> Maybe Symbol
forall a. Maybe a
Nothing
                          (OMDoc.CSy symbol :: Symbol
symbol : _) -> Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just Symbol
symbol
                          _ -> String -> Maybe Symbol
forall a. HasCallStack => String -> a
error "OMDoc.Logic_OMDoc.symmap_of"
                      msymbol2 :: Maybe Symbol
msymbol2 =
                        case
                          (Constitutive -> Bool) -> [Constitutive] -> [Constitutive]
forall a. (a -> Bool) -> [a] -> [a]
filter
                            (\ c :: Constitutive
c ->
                              case Constitutive
c of
                                (OMDoc.CSy symbol :: Symbol
symbol) ->
                                  Symbol -> String
OMDoc.symbolId Symbol
symbol String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
name2
                                _ ->
                                  Bool
False
                            )
                            (OMDoc_Sign -> [Constitutive]
OMDoc.theoryConstitutives OMDoc_Sign
s2)
                        of
                          [] -> Maybe Symbol
forall a. Maybe a
Nothing
                          (OMDoc.CSy symbol :: Symbol
symbol : _) -> Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just Symbol
symbol
                          _ -> String -> Maybe Symbol
forall a. HasCallStack => String -> a
error "OMDoc.Logic_OMDoc.symmap_of"
                      newmap :: EndoMap Symbol
newmap =
                        case (Maybe Symbol
msymbol1, Maybe Symbol
msymbol2) of
                          (Nothing, _) -> EndoMap Symbol
smap
                          (_, Nothing) -> EndoMap Symbol
smap
                          (Just symbol1 :: Symbol
symbol1, Just symbol2 :: Symbol
symbol2) ->
                            Symbol -> Symbol -> EndoMap Symbol -> EndoMap Symbol
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Symbol
symbol1 Symbol
symbol2 EndoMap Symbol
smap
                    in
                      EndoMap Symbol
newmap
                  _ -> EndoMap Symbol
smap
              _ ->
                EndoMap Symbol
smap
          )
          EndoMap Symbol
forall k a. Map k a
Map.empty
          (Morphism -> [(MText, MText)]
OMDoc.morphismRequations Morphism
im)
  sym_name :: OMDoc_PUN -> Symbol -> Id
sym_name OMDoc_PUN s :: Symbol
s =
    -- real Id's are saved as Presentation-Elements...
    String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ Symbol -> String
OMDoc.symbolId Symbol
s
  symKind :: OMDoc_PUN -> Symbol -> String
symKind OMDoc_PUN = SymbolRole -> String
forall a. Show a => a -> String
show (SymbolRole -> String)
-> (Symbol -> SymbolRole) -> Symbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> SymbolRole
OMDoc.symbolRole

instance StaticAnalysis OMDoc_PUN () () () () OMDoc_Sign OMDoc_Morphism OMDoc.Symbol () where
  symbol_to_raw :: OMDoc_PUN -> Symbol -> ()
symbol_to_raw OMDoc_PUN _ = ()
  id_to_raw :: OMDoc_PUN -> Id -> ()
id_to_raw OMDoc_PUN _ = ()
  matches :: OMDoc_PUN -> Symbol -> () -> Bool
matches OMDoc_PUN _ _ = Bool
False
  empty_signature :: OMDoc_PUN -> OMDoc_Sign
empty_signature OMDoc_PUN =
    Theory :: String
-> [Constitutive] -> [Presentation] -> Maybe String -> OMDoc_Sign
OMDoc.Theory
    {
        theoryId :: String
OMDoc.theoryId = "empty"
      , theoryConstitutives :: [Constitutive]
OMDoc.theoryConstitutives = []
      , theoryPresentations :: [Presentation]
OMDoc.theoryPresentations = []
      , theoryComment :: Maybe String
OMDoc.theoryComment = Maybe String
forall a. Maybe a
Nothing
    }

is_subsig :: OMDoc.Theory -> OMDoc.Theory -> Bool
is_subsig :: OMDoc_Sign -> OMDoc_Sign -> Bool
is_subsig s1 :: OMDoc_Sign
s1 s2 :: OMDoc_Sign
s2 =
    -- This currently only checks symbols. Maybe ADTs should also be checked...
    let
      s1sym :: Set Symbol
s1sym =
        (Set Symbol -> Constitutive -> Set Symbol)
-> Set Symbol -> [Constitutive] -> Set Symbol
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
          (\ s :: Set Symbol
s con :: Constitutive
con ->
            case Constitutive
con of
              (OMDoc.CSy sym :: Symbol
sym) ->
                Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => a -> Set a -> Set a
Set.insert Symbol
sym Set Symbol
s
              _ ->
                Set Symbol
s
          )
          Set Symbol
forall a. Set a
Set.empty
          (OMDoc_Sign -> [Constitutive]
OMDoc.theoryConstitutives OMDoc_Sign
s1)
      s2sym :: Set Symbol
s2sym =
        (Set Symbol -> Constitutive -> Set Symbol)
-> Set Symbol -> [Constitutive] -> Set Symbol
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
          (\ s :: Set Symbol
s con :: Constitutive
con ->
            case Constitutive
con of
              (OMDoc.CSy sym :: Symbol
sym) ->
                Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => a -> Set a -> Set a
Set.insert Symbol
sym Set Symbol
s
              _ ->
                Set Symbol
s
          )
          Set Symbol
forall a. Set a
Set.empty
          (OMDoc_Sign -> [Constitutive]
OMDoc.theoryConstitutives OMDoc_Sign
s2)
    in
     Set Symbol -> Set Symbol -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set Symbol
s1sym Set Symbol
s2sym

instance Logic OMDoc_PUN () () () () () OMDoc_Sign OMDoc_Morphism OMDoc.Symbol () ()