content: {-# LANGUAGE CPP, MultiParamTypeClasses #-}
  {-
  the following code is automatically generated by
      MMT/hets-mmt-standalone.jar
  static analysis is performed by MMT,
      therefore static analysis functions are absent
  -}
  module PLpatt.Logic_PLpatt where
  
  import Logic.Logic -- Logic and accompanying classes
  
  import qualified PLpatt.Sign as Sign
  import qualified PLpatt.Morphism as Morphism
  import qualified PLpatt.AS_BASIC_PLpatt as AS
  -- import qualified PLpatt.Tools as Tools -- TODO
  import qualified MMT.Tools as Generic
  -- import qualified PLpatt.Sublogic as SL -- TODO
  import Common.Id
  import qualified Common.DocUtils as DU
  import qualified Common.Doc as DU
  import qualified ATerm.Conversion as AT
  import qualified Data.Typeable.Internal as Tp
  import Common.Result
  import Data.Monoid
  import qualified PLpatt.Parse_PLpatt as LogicParse
  import PLpatt.StaticAnaPLpatt
  
  -- Logic ID     lid
  data PLpatt = PLpatt deriving Show
  
  -- language
  instance Language PLpatt where
      description _ = "This is some logic generated by MMT\n"
  
  instance (Ord Sign.Sigs) where
  
  instance (Eq Sign.Sigs) where
  
  instance (Ord Morphism.Morphism) where
  
  instance (Eq Morphism.Morphism) where
    _ == _ = True
  
  instance (Common.Id.GetRange AS.Bool') where
  
  instance (Common.Id.GetRange AS.Symb) where
  
  instance (DU.Pretty Sign.Sigs) where
      pretty a = DU.text $ show a
  
  instance (AT.ShATermConvertible Sign.Sigs) where
      toShATermAux = AT.toShATermAux
      fromShATermAux = AT.fromShATermAux
  
  instance (AT.ShATermConvertible Generic.Tree) where
      toShATermAux = AT.toShATermAux
      fromShATermAux = AT.fromShATermAux
  
  instance (Ord Generic.Tree) where
    _ <= _ = True
  
  instance (Eq Generic.Tree) where
    _ == _ = True
  
  instance (AT.ShATermConvertible Morphism.Morphism) where
      toShATermAux = AT.toShATermAux
      fromShATermAux = AT.fromShATermAux
  
  instance (DU.Pretty Morphism.Morphism) where
      pretty a = DU.text $ show a
  
  instance (AT.ShATermConvertible AS.Bool') where
      toShATermAux = AT.toShATermAux
      fromShATermAux = AT.fromShATermAux
  
  instance (DU.Pretty AS.Bool') where
      pretty a = DU.text $ show a
  
  instance (AT.ShATermConvertible AS.Symb) where
      toShATermAux = AT.toShATermAux
      fromShATermAux = AT.fromShATermAux
  
  instance (DU.Pretty AS.Symb) where
      pretty a = DU.text $ show $ AS.sname a
  
  instance (Show Morphism.Morphism) where
  
  instance (Tp.Typeable Morphism.Morphism) where
      typeOf = Tp.typeOf
  
  instance (DU.Pretty AS.Basic_spec) where
      pretty a = DU.text $ case a of (AS.Basic_spec ls) -> unlines ls
  
  instance (GetRange AS.Basic_spec) where
  
  instance (Data.Monoid.Monoid AS.Basic_spec) where
      mempty = AS.Basic_spec []
      mappend (AS.Basic_spec bs1) (AS.Basic_spec bs2) = AS.Basic_spec $ bs1 ++ bs2
  
  instance (AT.ShATermConvertible AS.Basic_spec) where
      toShATermAux = AT.toShATermAux
      fromShATermAux = AT.fromShATermAux
  
  -- static analysis should in fact be performed by MMT
  instance StaticAnalysis PLpatt
              AS.Basic_spec -- datatype for syntax trees - Generic.Tree?
              AS.Bool'
              ()
              ()
              Sign.Sigs
              Morphism.Morphism
              AS.Symb
              AS.Symb
                  where
              empty_signature PLpatt = Sign.Sigs []
              signatureDiff PLpatt = Sign.sigDiff
              basic_analysis PLpatt = Just basicAna
  
  instance Syntax PLpatt
                  AS.Basic_spec -- parse_basic_spec produces a syntax tree
                  AS.Symb
                  ()
                  ()
                      where
    parse_basic_spec _ = Just $ const LogicParse.parse1
  -- basic_analysis lid = Just (\ ..  )
  
  -- instance of category
  instance Category Sign.Sigs Morphism.Morphism where
      ide sgn = Morphism.Morphism sgn sgn
      composeMorphisms mor1 _ = Result [] (Just mor1) -- TODO
      dom = Morphism.source
      cod = Morphism.target
  
  instance Sentences PLpatt
      AS.Bool'
      Sign.Sigs
      Morphism.Morphism
      AS.Symb
      where
  
  -- Logic instance, see Logic/Logic.hs:867
  instance Logic PLpatt
      () -- SL.Sublogic -- sublogic
      AS.Basic_spec -- basic_spec
      AS.Bool'
      () -- symb_items
      () -- symb_map_items
      Sign.Sigs -- sign
      Morphism.Morphism  -- sentence
      AS.Symb -- Symb
      AS.Symb -- raw Symb
      () -- proof tree
      where
   {-
   logic_name = show
   id lid = Morphism.id
   comp lid = Morphism.comp
   parse_basic_spec lid = Generic.parseSpec
   map_sen lid = Morphism.mapSen
   basic_analysis lid = Tools.theo_from_pt
   stat_symb_map lid = Tools.mor_from_pt
   minSublogic lid = SL.minSublogic
  -}
  