{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE MonoLocalBinds #-}
{- |
Module      :  ./Logic/Logic.hs
Description :  central interface (type class) for logics in Hets
Copyright   :  (c) Till Mossakowski, and Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (various -fglasgow-exts extensions)

Central interface (type class) for logics in Hets

Provides data structures for logics (with symbols). Logics are
   a type class with an /identity type/ (usually interpreted
   by a singleton set) which serves to treat logics as
   data. All the functions in the type class take the
   identity as first argument in order to determine the logic.

   For logic (co)morphisms see "Logic.Comorphism"

   This module uses multiparameter type classes with functional dependencies
   (<http://www.haskell.org/haskellwiki/Functional_dependencies>)
   for defining an interface for the notion of logic. Multiparameter type
   classes are needed because a logic consists of a collection of types,
   together with operations on these. Functional dependencies
   are needed because no operation will involve all types of
   the multiparameter type class; hence we need a method to derive
   the missing types. We chose an easy way: for each logic, we
   introduce a new singleton type that is the name, or constitutes the identity
   of the logic. All other types of the multiparameter type class
   depend on this /identity constituting/ type, and all operations take
   the 'identity constituting' type as first arguments. The value
   of the argument of the /identity constituting/ type is irrelevant
   (note that there is only one value of such a type anyway).

   Note that we tend to use @lid@ both for the /identity type/
   of a logic, as well as for its unique inhabitant, i.e. @lid :: lid@.

   The other types involved in the definition of logic are as follows:

   * sign: signatures, that is, contexts, or non-logical vocabularies,
   typically consisting of a set of declared sorts, predicates,
   function symbols, propositional letters etc., together with their
   typing.

   * sentence: logical formulas.

   * basic_spec: abstract syntax of basic specifications. The latter are
   human-readable presentations of a signature together with some sentences.

   * symbol: symbols that may occur in a signature, fully qualified
   with their types

   * raw_symbol:  symbols that may occur in a signature, possibly not
   or partially qualified

   * morphism: maps between signatures (typically preserving the structure).

   * symb_items: abstract syntax of symbol lists, used for declaring some
   symbols of a signature as hidden.

   * symb_map_items: abstract syntax of symbol maps, i.e. human-readable
   presentations of signature morphisms.

   * sublogics: sublogics of the given logic. This type might be a
   record of Boolean flags, indicating whether some feature is
   present in the sublogi of not.

   * proof_tree: proof trees.

   References:

   J. A. Goguen and R. M. Burstall
   Institutions: Abstract Model Theory for Specification and
     Programming
   JACM 39, p. 95-146, 1992
   (general notion of logic - model theory only)

   J. Meseguer
   General Logics
   Logic Colloquium 87, p. 275-329, North Holland, 1989
   (general notion of logic - also proof theory;
    notion of logic representation, called map there)

   T. Mossakowski:
   Specification in an arbitrary institution with symbols
   14th WADT 1999, LNCS 1827, p. 252-270
   (treatment of symbols and raw symbols, see also CASL semantics
    in the CASL reference manual)

   T. Mossakowski, B. Klin:
   Institution Independent Static Analysis for CASL
   15h WADT 2001, LNCS 2267, p. 221-237, 2002.
   (what is needed for static anaylsis)

   S. Autexier and T. Mossakowski
   Integrating HOLCASL into the Development Graph Manager MAYA
   FroCoS 2002, LNCS 2309, p. 2-17, 2002.
   (interface to provers)

   CoFI (ed.): CASL Reference Manual, LNCS 2960, Springer Verlag, 2004.
   (static semantics of CASL structured and architectural specifications)

   T. Mossakowski
   Heterogeneous specification and the heterogeneous tool set
   Habilitation thesis, University of Bremen, 2005
   (the general picture of heterogeneous specification)
-}

module Logic.Logic where

import Logic.Prover (Prover, ConsChecker, Theory (..))
import Logic.KnownIris

import Taxonomy.MMiSSOntology (MMiSSOntology)

import ATC.DefaultMorphism ()

import qualified OMDoc.DataTypes as OMDoc
  ( TCElement
  , TCorOMElement
  , NameMap
  , SigMap
  , SigMapI
  , OMCD
  , OmdADT)

import ATerm.Lib (ShATermConvertible)

import Common.AS_Annotation
import Common.Amalgamate
import Common.AnnoState
import Common.Consistency
import Common.DefaultMorphism
import Common.Doc
import Common.DocUtils
import Common.ExtSign
import Common.GlobalAnnotations
import Common.Id
import Common.IRI
import Common.Item
import Common.Json
import Common.Lib.Graph
import Common.LibName
import Common.Prec (PrecMap)
import Common.Result
import Common.Taxonomy
import Common.ToXml

import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.Monoid ()
import Data.Ord
import Data.Typeable
import Control.Monad (unless)
import qualified Control.Monad.Fail as Fail

import Data.Aeson (FromJSON, ToJSON)

-- | Stability of logic implementations
data Stability = Stable | Testing | Unstable | Experimental
     deriving (Stability -> Stability -> Bool
(Stability -> Stability -> Bool)
-> (Stability -> Stability -> Bool) -> Eq Stability
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Stability -> Stability -> Bool
$c/= :: Stability -> Stability -> Bool
== :: Stability -> Stability -> Bool
$c== :: Stability -> Stability -> Bool
Eq, Int -> Stability -> ShowS
[Stability] -> ShowS
Stability -> String
(Int -> Stability -> ShowS)
-> (Stability -> String)
-> ([Stability] -> ShowS)
-> Show Stability
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Stability] -> ShowS
$cshowList :: [Stability] -> ShowS
show :: Stability -> String
$cshow :: Stability -> String
showsPrec :: Int -> Stability -> ShowS
$cshowsPrec :: Int -> Stability -> ShowS
Show)

-- | shortcut for class constraints
class ShATermConvertible a => Convertible a
instance ShATermConvertible a => Convertible a

-- | shortcut for class constraints
class (Pretty a, Convertible a, ToJSON a, FromJSON a) => PrintTypeConv a
instance (Pretty a, Convertible a, ToJSON a, FromJSON a) => PrintTypeConv a

-- | shortcut for class constraints with equality
class (Eq a, PrintTypeConv a) => EqPrintTypeConv a
instance (Eq a, PrintTypeConv a) => EqPrintTypeConv a

-- | maps from a to a
type EndoMap a = Map.Map a a

{- | the name of a logic.
     Define instances like "data CASL = CASL deriving (Show, Typeable, Data)"
-}
class Show lid => Language lid where
    language_name :: lid -> String
    language_name = lid -> String
forall a. Show a => a -> String
show
    description :: lid -> String
    -- default implementation
    description _ = ""

-- short description = first line of description
short_description :: Language lid => lid -> String
short_description :: lid -> String
short_description l :: lid
l = [String] -> String
forall a. [a] -> a
head ((String -> [String]
lines (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ lid -> String
forall lid. Language lid => lid -> String
description lid
l) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [""])
      
{- | Categories are given as usual: objects, morphisms, identities,
     domain, codomain and composition. The type id is the name, or
     the identity of the category. It is an argument to all functions
     of the type class, serving disambiguation among instances
     (via the functional dependency lid -> object morphism).
     The types for objects and morphisms may be restricted to
     subtypes, using legal_obj and legal_mor. For example, for the
     category of sets and injective maps, legal_mor would check
     injectivity. Since Eq is a subclass of Category, it is also
     possible to impose a quotient on the types for objects and morphisms.
     Require Ord instances only for efficiency, i.e. in sets or maps.
-}
class (Ord object, Ord morphism)
    => Category object morphism | morphism -> object where
         -- | identity morphisms
         ide :: object -> morphism
         {- | composition, in diagrammatic order,
         if intermediate objects are equal (not checked!) -}
         composeMorphisms :: morphism -> morphism -> Result morphism
         -- | domain and codomain of morphisms
         dom, cod :: morphism -> object
         -- | the inverse of a morphism
         inverse :: morphism -> Result morphism
         inverse _ = String -> Result morphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Logic.Logic.Category.inverse not implemented"
         -- | test if the signature morphism an inclusion
         isInclusion :: morphism -> Bool
         isInclusion _ = Bool
False -- in general no inclusion

         -- | is a value of type morphism denoting a legal  morphism?
         legal_mor :: morphism -> Result ()
         legal_mor _ = () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | test if the signature morphism is the identity
isIdentity :: Category object morphism => morphism -> Bool
isIdentity :: morphism -> Bool
isIdentity m :: morphism
m = morphism -> Bool
forall object morphism.
Category object morphism =>
morphism -> Bool
isInclusion morphism
m Bool -> Bool -> Bool
&& morphism -> object
forall object morphism.
Category object morphism =>
morphism -> object
dom morphism
m object -> object -> Bool
forall a. Eq a => a -> a -> Bool
== morphism -> object
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
m

comp :: Category object morphism => morphism -> morphism -> Result morphism
comp :: morphism -> morphism -> Result morphism
comp m1 :: morphism
m1 m2 :: morphism
m2 = if morphism -> object
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
m1 object -> object -> Bool
forall a. Eq a => a -> a -> Bool
== morphism -> object
forall object morphism.
Category object morphism =>
morphism -> object
dom morphism
m2 then morphism -> morphism -> Result morphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
composeMorphisms morphism
m1 morphism
m2 else
  String -> Result morphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "target of first and source of second morphism are different"

instance Ord sign => Category sign (DefaultMorphism sign) where
    dom :: DefaultMorphism sign -> sign
dom = DefaultMorphism sign -> sign
forall sign. DefaultMorphism sign -> sign
domOfDefaultMorphism
    cod :: DefaultMorphism sign -> sign
cod = DefaultMorphism sign -> sign
forall sign. DefaultMorphism sign -> sign
codOfDefaultMorphism
    ide :: sign -> DefaultMorphism sign
ide = sign -> DefaultMorphism sign
forall sign. sign -> DefaultMorphism sign
ideOfDefaultMorphism
    isInclusion :: DefaultMorphism sign -> Bool
isInclusion = Bool -> DefaultMorphism sign -> Bool
forall a b. a -> b -> a
const Bool
True
    composeMorphisms :: DefaultMorphism sign
-> DefaultMorphism sign -> Result (DefaultMorphism sign)
composeMorphisms = DefaultMorphism sign
-> DefaultMorphism sign -> Result (DefaultMorphism sign)
forall (m :: * -> *) sign.
Monad m =>
DefaultMorphism sign
-> DefaultMorphism sign -> m (DefaultMorphism sign)
compOfDefaultMorphism

{- | Abstract syntax, parsing and printing.
     There are three types for abstract syntax:
     basic_spec is for basic specifications (see CASL RefMan p. 5ff.),
     symb_items is for symbol lists (see CASL RefMan p. 35ff.),
     symb_map_items is for symbol maps (see CASL RefMan p. 35ff.).
-}
class (Language lid, PrintTypeConv basic_spec, GetRange basic_spec,
       Monoid basic_spec, -- for joining converted signatures and sentences
       Pretty symbol,
       EqPrintTypeConv symb_items,
       EqPrintTypeConv symb_map_items)
    => Syntax lid basic_spec symbol symb_items symb_map_items
        | lid -> basic_spec symbol symb_items symb_map_items
      where
         -- | parsers and printers
         parsersAndPrinters :: lid -> Map.Map String
            (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
         parsersAndPrinters li :: lid
li = case lid -> Maybe (PrefixMap -> AParser st basic_spec)
forall lid basic_spec symbol symb_items symb_map_items st.
Syntax lid basic_spec symbol symb_items symb_map_items =>
lid -> Maybe (PrefixMap -> AParser st basic_spec)
parse_basic_spec lid
li of
            Nothing -> Map String (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
forall k a. Map k a
Map.empty
            Just p :: PrefixMap -> AParser st basic_spec
p -> (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
-> Map
     String (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
forall b. b -> Map String b
makeDefault (PrefixMap -> AParser st basic_spec
p, basic_spec -> Doc
forall a. Pretty a => a -> Doc
pretty)
         -- | parser for basic specifications
         parse_basic_spec :: lid -> Maybe (PrefixMap -> AParser st basic_spec)
         -- | parser for a single symbol returned as list
         parseSingleSymbItem :: lid -> Maybe (PrefixMap -> AParser st symb_items)
         -- | parser for symbol lists
         parse_symb_items :: lid -> Maybe (PrefixMap -> AParser st symb_items)
         -- | parser for symbol maps
         parse_symb_map_items :: lid -> Maybe (PrefixMap -> AParser st symb_map_items)
         toItem :: lid -> basic_spec -> Item
         symb_items_name :: lid -> symb_items -> [String]
         -- default implementations
         parse_basic_spec _ = Maybe (PrefixMap -> AParser st basic_spec)
forall a. Maybe a
Nothing
         parseSingleSymbItem _ = Maybe (PrefixMap -> AParser st symb_items)
forall a. Maybe a
Nothing
         parse_symb_items _ = Maybe (PrefixMap -> AParser st symb_items)
forall a. Maybe a
Nothing
         parse_symb_map_items _ = Maybe (PrefixMap -> AParser st symb_map_items)
forall a. Maybe a
Nothing
         symb_items_name _ _ = [""]
         toItem _ bs :: basic_spec
bs = (String, Doc) -> Range -> Item
forall a. ItemTypeable a => a -> Range -> Item
mkFlatItem ("Basicspec", basic_spec -> Doc
forall a. Pretty a => a -> Doc
pretty basic_spec
bs) (Range -> Item) -> Range -> Item
forall a b. (a -> b) -> a -> b
$ basic_spec -> Range
forall a. GetRange a => a -> Range
getRangeSpan basic_spec
bs

basicSpecParser :: Syntax lid basic_spec symbol symb_items symb_map_items
  => Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec)
basicSpecParser :: Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec)
basicSpecParser sm :: Maybe IRI
sm = ((PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
 -> PrefixMap -> AParser st basic_spec)
-> Maybe (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
-> Maybe (PrefixMap -> AParser st basic_spec)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
-> PrefixMap -> AParser st basic_spec
forall a b. (a, b) -> a
fst (Maybe (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
 -> Maybe (PrefixMap -> AParser st basic_spec))
-> (lid
    -> Maybe (PrefixMap -> AParser st basic_spec, basic_spec -> Doc))
-> lid
-> Maybe (PrefixMap -> AParser st basic_spec)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe IRI
-> lid
-> Maybe (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
forall lid basic_spec symbol symb_items symb_map_items st.
Syntax lid basic_spec symbol symb_items symb_map_items =>
Maybe IRI
-> lid
-> Maybe (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
parserAndPrinter Maybe IRI
sm

basicSpecPrinter :: Syntax lid basic_spec symbol symb_items symb_map_items
  => Maybe IRI -> lid -> Maybe (basic_spec -> Doc)
basicSpecPrinter :: Maybe IRI -> lid -> Maybe (basic_spec -> Doc)
basicSpecPrinter sm :: Maybe IRI
sm = ((PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
 -> basic_spec -> Doc)
-> Maybe (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
-> Maybe (basic_spec -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
-> basic_spec -> Doc
forall a b. (a, b) -> b
snd (Maybe (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
 -> Maybe (basic_spec -> Doc))
-> (lid
    -> Maybe (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc))
-> lid
-> Maybe (basic_spec -> Doc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe IRI
-> lid
-> Maybe (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
forall lid basic_spec symbol symb_items symb_map_items st.
Syntax lid basic_spec symbol symb_items symb_map_items =>
Maybe IRI
-> lid
-> Maybe (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
parserAndPrinter Maybe IRI
sm

basicSpecSyntaxes :: Syntax lid basic_spec symbol symb_items symb_map_items
  => lid -> [String]
basicSpecSyntaxes :: lid -> [String]
basicSpecSyntaxes = Map String String -> [String]
forall k a. Map k a -> [k]
Map.keys (Map String String -> [String])
-> (lid -> Map String String) -> lid -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Map String String
serializations (String -> Map String String)
-> (lid -> String) -> lid -> Map String String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. lid -> String
forall lid. Language lid => lid -> String
language_name

parserAndPrinter :: Syntax lid basic_spec symbol symb_items symb_map_items
  => Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec,
                                basic_spec -> Doc)
parserAndPrinter :: Maybe IRI
-> lid
-> Maybe (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
parserAndPrinter sm :: Maybe IRI
sm l :: lid
l = lid
-> Maybe IRI
-> Map
     String (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
-> Maybe (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
forall lid basic_spec symbol symb_items symb_map_items b.
Syntax lid basic_spec symbol symb_items symb_map_items =>
lid -> Maybe IRI -> Map String b -> Maybe b
lookupDefault lid
l Maybe IRI
sm (lid
-> Map
     String (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
forall lid basic_spec symbol symb_items symb_map_items st.
Syntax lid basic_spec symbol symb_items symb_map_items =>
lid
-> Map
     String (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
parsersAndPrinters lid
l)

-- | function to lookup parser or printer
lookupDefault :: Syntax lid basic_spec symbol symb_items symb_map_items
  => lid -> Maybe IRI -> Map.Map String b -> Maybe b
lookupDefault :: lid -> Maybe IRI -> Map String b -> Maybe b
lookupDefault l :: lid
l im :: Maybe IRI
im m :: Map String b
m = case Maybe IRI
im of
     Just i :: IRI
i -> do
       let s :: String
s = IRI -> String
iriToStringUnsecure IRI
i
       String
ser <- if IRI -> Bool
isSimple IRI
i then String -> Maybe String
forall (m :: * -> *) a. Monad m => a -> m a
return String
s
              else String -> String -> Maybe String
lookupSerialization (lid -> String
forall lid. Language lid => lid -> String
language_name lid
l) String
s
       String -> Map String b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
ser Map String b
m
     Nothing -> if Map String b -> Int
forall k a. Map k a -> Int
Map.size Map String b
m Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then b -> Maybe b
forall a. a -> Maybe a
Just (b -> Maybe b) -> b -> Maybe b
forall a b. (a -> b) -> a -> b
$ [b] -> b
forall a. [a] -> a
head ([b] -> b) -> [b] -> b
forall a b. (a -> b) -> a -> b
$ Map String b -> [b]
forall k a. Map k a -> [a]
Map.elems Map String b
m
                else String -> Map String b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup "" Map String b
m

showSyntax :: Language lid => lid -> Maybe IRI -> String
showSyntax :: lid -> Maybe IRI -> String
showSyntax lid :: lid
lid = (("logic " String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid) String -> ShowS
forall a. [a] -> [a] -> [a]
++)
   ShowS -> (Maybe IRI -> String) -> Maybe IRI -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> (IRI -> String) -> Maybe IRI -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" ((" serialization " String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> (IRI -> String) -> IRI -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> String
iriToStringUnsecure)

makeDefault :: b -> Map.Map String b
makeDefault :: b -> Map String b
makeDefault = String -> b -> Map String b
forall k a. k -> a -> Map k a
Map.singleton ""

addSyntax :: String -> b -> Map.Map String b -> Map.Map String b
addSyntax :: String -> b -> Map String b -> Map String b
addSyntax = String -> b -> Map String b -> Map String b
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert

{- | Sentences, provers and symbols.
     Provers capture the entailment relation between sets of sentences
     and sentences. They may return proof trees witnessing proofs.
     Signatures are equipped with underlying sets of symbols
     (such that the category of signatures becomes a concrete category),
     see CASL RefMan p. 191ff.
-}
class (Language lid, Category sign morphism, Ord sentence,
       Ord symbol, -- for efficient lookup
       PrintTypeConv sign, PrintTypeConv morphism,
       GetRange sentence, GetRange symbol,
       PrintTypeConv sentence, ToJson sentence,
       ToXml sentence, PrintTypeConv symbol)
    => Sentences lid sentence sign morphism symbol
        | lid -> sentence sign morphism symbol
      where

      -- | sentence translation along a signature morphism
      map_sen :: lid -> morphism -> sentence -> Result sentence
      map_sen l :: lid
l _ _ = lid -> String -> Result sentence
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "map_sen"

      -- | simplification of sentences (leave out qualifications)
      simplify_sen :: lid -> sign -> sentence -> sentence
      simplify_sen _ _ = sentence -> sentence
forall a. a -> a
id

      -- | negation of a sentence for disproving
      negation :: lid -> sentence -> Maybe sentence
      negation _ _ = Maybe sentence
forall a. Maybe a
Nothing

      -- | modified signature printing when followed by sentences
      print_sign :: lid -> sign -> Doc
      print_sign _ = sign -> Doc
forall a. Pretty a => a -> Doc
pretty

      -- | print a sentence with comments
      print_named :: lid -> Named sentence -> Doc
      print_named _ = (sentence -> Doc) -> Annoted sentence -> Doc
forall a. (a -> Doc) -> Annoted a -> Doc
printAnnoted (Doc -> Doc
addBullet (Doc -> Doc) -> (sentence -> Doc) -> sentence -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sentence -> Doc
forall a. Pretty a => a -> Doc
pretty) (Annoted sentence -> Doc)
-> (Named sentence -> Annoted sentence) -> Named sentence -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named sentence -> Annoted sentence
forall s. Named s -> Annoted s
fromLabelledSen

      -- --------------------- symbols ---------------------------

      -- | dependency ordered list of symbol sets for a signature
      sym_of :: lid -> sign -> [Set.Set symbol]
      sym_of _ _ = []
      {- | Dependency ordered list of a bigger symbol set for a
      signature. This function contains more symbols than those being subject
      to hiding and renaming (given by 'sym_of') to better represent a
      signature as a set of symbols given within xml files. At least for CASL
      additional symbols for (direct) subsorts will be created, but note, that
      no symbol for a partial function will be created, if the signature
      contains this function as total, although a signature with just that
      partial function would be a subsignature. This function is supposed to
      work over partial signatures created by 'signatureDiff'. -}
      mostSymsOf :: lid -> sign -> [symbol]
      mostSymsOf l :: lid
l = (Set symbol -> [symbol]) -> [Set symbol] -> [symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Set symbol -> [symbol]
forall a. Set a -> [a]
Set.toList ([Set symbol] -> [symbol])
-> (sign -> [Set symbol]) -> sign -> [symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. lid -> sign -> [Set symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> [Set symbol]
sym_of lid
l

      -- | symbol map for a signature morphism
      symmap_of :: lid -> morphism -> EndoMap symbol
      symmap_of _ _ = EndoMap symbol
forall k a. Map k a
Map.empty
      -- | symbols have a name, see CASL RefMan p. 192
      sym_name :: lid -> symbol -> Id
      sym_name l :: lid
l _ = lid -> String -> Id
forall lid a. Language lid => lid -> String -> a
statError lid
l "sym_name"
      -- | some symbols have a label for better readability
      sym_label :: lid -> symbol -> Maybe String
      sym_label _ _ = Maybe String
forall a. Maybe a
Nothing
      -- | the fully qualified name for XML output (i.e. of OWL2)
      fullSymName :: lid -> symbol -> String
      fullSymName l :: lid
l = Id -> String
forall a. Show a => a -> String
show (Id -> String) -> (symbol -> Id) -> symbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. lid -> symbol -> Id
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Id
sym_name lid
l
      -- | a logic dependent kind of a symbol
      symKind :: lid -> symbol -> String
      symKind _ _ = "defaultKind"
      -- | the symbols occuring in a sentence (any order)
      symsOfSen :: lid -> sign -> sentence -> [symbol]
      symsOfSen _ _ _ = []
      -- | combine two symbols into another one
      pair_symbols :: lid -> symbol -> symbol -> Result symbol
      pair_symbols lid :: lid
lid _ _ = String -> Result symbol
forall a. HasCallStack => String -> a
error (String -> Result symbol) -> String -> Result symbol
forall a b. (a -> b) -> a -> b
$ "pair_symbols nyi for logic " String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid -> String
forall a. Show a => a -> String
show lid
lid

-- | makes a singleton list from the given value
singletonList :: a -> [a]
singletonList :: a -> [a]
singletonList x :: a
x = [a
x]

-- | set of symbols for a signature
symset_of :: forall lid sentence sign morphism symbol .
             Sentences lid sentence sign morphism symbol =>
             lid -> sign -> Set.Set symbol
symset_of :: lid -> sign -> Set symbol
symset_of lid :: lid
lid sig :: sign
sig = [Set symbol] -> Set symbol
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set symbol] -> Set symbol) -> [Set symbol] -> Set symbol
forall a b. (a -> b) -> a -> b
$ lid -> sign -> [Set symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> [Set symbol]
sym_of lid
lid sign
sig

-- | dependency ordered list of symbols for a signature
symlist_of :: forall lid sentence sign morphism symbol .
              Sentences lid sentence sign morphism symbol =>
              lid -> sign -> [symbol]
symlist_of :: lid -> sign -> [symbol]
symlist_of lid :: lid
lid sig :: sign
sig = (Set symbol -> [symbol]) -> [Set symbol] -> [symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Set symbol -> [symbol]
forall a. Set a -> [a]
Set.toList ([Set symbol] -> [symbol]) -> [Set symbol] -> [symbol]
forall a b. (a -> b) -> a -> b
$ lid -> sign -> [Set symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> [Set symbol]
sym_of lid
lid sign
sig

-- | a dummy static analysis function to allow type checking *.inline.hs files
inlineAxioms :: StaticAnalysis lid
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol => lid -> String -> [Named sentence]
inlineAxioms :: lid -> String -> [Named sentence]
inlineAxioms _ _ = String -> [Named sentence]
forall a. HasCallStack => String -> a
error "inlineAxioms"

-- | fail function for static analysis
statFail :: (Language lid, Fail.MonadFail m) => lid -> String -> m a
statFail :: lid -> String -> m a
statFail lid :: lid
lid = String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m a) -> ShowS -> String -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. lid -> ShowS
forall lid. Language lid => lid -> ShowS
statErrMsg lid
lid

statError :: Language lid => lid -> String -> a
statError :: lid -> String -> a
statError lid :: lid
lid = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> ShowS -> String -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. lid -> ShowS
forall lid. Language lid => lid -> ShowS
statErrMsg lid
lid

-- | error message for static analysis
statErrMsg :: Language lid => lid -> String -> String
statErrMsg :: lid -> ShowS
statErrMsg lid :: lid
lid str :: String
str =
  "Logic." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ " not implemented for: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid

{- static analysis
   This type class provides the data needed for an institution with symbols,
   as explained in the structured specification semantics in the CASL
   reference manual, chapter III.4.
   The static analysis computes signatures from basic specifications,
   and signature morphisms from symbol lists and symbol maps. The latter
   needs an intermediate stage, so-called raw symbols, which are possibly
   unqualified symbols. Normal symbols are always fully qualified.
   In the CASL reference manual, our symbols are called "signature symbols",
   and our raw symbols are called "symbols". (Terminology should be adapted.)
-}

data REL_REF = Subs | IsSubs | Equiv | Incomp
                  | HasInst | InstOf | DefRel
                  | RelName IRI
                    deriving (Int -> REL_REF -> ShowS
[REL_REF] -> ShowS
REL_REF -> String
(Int -> REL_REF -> ShowS)
-> (REL_REF -> String) -> ([REL_REF] -> ShowS) -> Show REL_REF
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [REL_REF] -> ShowS
$cshowList :: [REL_REF] -> ShowS
show :: REL_REF -> String
$cshow :: REL_REF -> String
showsPrec :: Int -> REL_REF -> ShowS
$cshowsPrec :: Int -> REL_REF -> ShowS
Show, REL_REF -> REL_REF -> Bool
(REL_REF -> REL_REF -> Bool)
-> (REL_REF -> REL_REF -> Bool) -> Eq REL_REF
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: REL_REF -> REL_REF -> Bool
$c/= :: REL_REF -> REL_REF -> Bool
== :: REL_REF -> REL_REF -> Bool
$c== :: REL_REF -> REL_REF -> Bool
Eq)

class ( Syntax lid basic_spec symbol symb_items symb_map_items
      , Sentences lid sentence sign morphism symbol
      , GetRange raw_symbol, Ord raw_symbol, Pretty raw_symbol
      , Typeable raw_symbol)
    => StaticAnalysis lid
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol
        | lid -> basic_spec sentence symb_items symb_map_items
                 sign morphism symbol raw_symbol
      where
         {- | static analysis of basic specifications and symbol maps.
            The resulting bspec has analyzed axioms in it.
            The resulting sign is an extension of the input sign
            plus newly declared or redeclared symbols.
            See CASL RefMan p. 138 ff. -}
         basic_analysis :: lid
           -> Maybe ((basic_spec, sign, GlobalAnnos)
             -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
         basic_analysis _ = Maybe
  ((basic_spec, sign, GlobalAnnos)
   -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
forall a. Maybe a
Nothing
         -- | Analysis of just sentences
         sen_analysis :: lid
           -> Maybe ((basic_spec, sign, sentence) -> Result sentence)
         sen_analysis _ = Maybe ((basic_spec, sign, sentence) -> Result sentence)
forall a. Maybe a
Nothing
         -- | a basic analysis with additional arguments
         extBasicAnalysis :: lid -> IRI -> LibName
             -> basic_spec -> sign -> GlobalAnnos
             -> Result (basic_spec, ExtSign sign symbol, [Named sentence])
         extBasicAnalysis l :: lid
l _ _ b :: basic_spec
b s :: sign
s g :: GlobalAnnos
g = case lid
-> Maybe
     ((basic_spec, sign, GlobalAnnos)
      -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid
-> Maybe
     ((basic_spec, sign, GlobalAnnos)
      -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
basic_analysis lid
l of
            Nothing -> lid
-> String
-> Result (basic_spec, ExtSign sign symbol, [Named sentence])
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "basic_analysis"
            Just ba :: (basic_spec, sign, GlobalAnnos)
-> Result (basic_spec, ExtSign sign symbol, [Named sentence])
ba -> (basic_spec, sign, GlobalAnnos)
-> Result (basic_spec, ExtSign sign symbol, [Named sentence])
ba (basic_spec
b, sign
s, GlobalAnnos
g)
         -- | static analysis of symbol maps, see CASL RefMan p. 222f.
         stat_symb_map_items :: lid -> sign -> Maybe sign -> [symb_map_items]
             -> Result (EndoMap raw_symbol)
         stat_symb_map_items l :: lid
l _ _ _ = lid -> String -> Result (EndoMap raw_symbol)
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "stat_symb_map_items"
         -- | static analysis of symbol lists, see CASL RefMan p. 221f.
         stat_symb_items :: lid -> sign -> [symb_items] -> Result [raw_symbol]
         stat_symb_items l :: lid
l _ _ = lid -> String -> Result [raw_symbol]
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "stat_symb_items"

         -- | convert a theory to basic specs for different serializations
         convertTheory :: lid -> Maybe ((sign, [Named sentence]) -> basic_spec)
         convertTheory _ = Maybe ((sign, [Named sentence]) -> basic_spec)
forall a. Maybe a
Nothing

         {- ----------------------- amalgamation ---------------------------
            Computation of colimits of signature diagram.
            Indeed, it suffices to compute a cocone that is weakly amalgamable
            see Till Mossakowski,
            Heterogeneous specification and the heterogeneous tool set
            p. 25ff. -}

         -- | architectural sharing analysis, see CASL RefMan p. 247ff.
         ensures_amalgamability :: lid ->
              ([CASLAmalgOpt],        -- the program options
               Gr sign (Int, morphism), -- the diagram to be analyzed
               [(Int, morphism)],     -- the sink
               Gr String String) -- the descriptions of nodes and edges
                  -> Result Amalgamates
         ensures_amalgamability l :: lid
l _ = Amalgamates -> String -> Range -> Result Amalgamates
forall a. a -> String -> Range -> Result a
warning Amalgamates
Amalgamates
           ("amalgamability test not implemented for logic " String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid -> String
forall a. Show a => a -> String
show lid
l)
           Range
nullRange
         -- | quotient term algebra for normalization of freeness
         quotient_term_algebra :: lid -- the logic
             -> morphism -- sigma : Sigma -> SigmaM
             -> [Named sentence] -- Th(M)
             -> Result
                 (sign, -- SigmaK
                  [Named sentence] -- Ax(K)
                 )
         quotient_term_algebra l :: lid
l _ _ = lid -> String -> Result (sign, [Named sentence])
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "quotient_term_algebra"
         -- | signature colimits
         signature_colimit :: lid -> Gr sign (Int, morphism)
                           -> Result (sign, Map.Map Int morphism)
         signature_colimit l :: lid
l _ = lid -> String -> Result (sign, Map Int morphism)
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "signature_colimit"
         {- | rename and qualify the symbols considering a united incoming
            morphisms, code out overloading and
            create sentences for the overloading relation -}
         qualify :: lid -> SIMPLE_ID -> LibName -> morphism -> sign
                 -> Result (morphism, [Named sentence])
         qualify l :: lid
l _ _ _ _ = lid -> String -> Result (morphism, [Named sentence])
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "qualify"

         -- ------------------ symbols and raw symbols ---------------------

         {- | Construe a symbol, like f:->t, as a raw symbol.
            This is a one-sided inverse to the function SymSySigSym
            in the CASL RefMan p. 192. -}
         symbol_to_raw :: lid -> symbol -> raw_symbol
         symbol_to_raw l :: lid
l _ = lid -> String -> raw_symbol
forall lid a. Language lid => lid -> String -> a
statError lid
l "symbol_to_raw"
         {- | Construe an identifier, like f, as a raw symbol.
            See CASL RefMan p. 192, function IDAsSym -}
         id_to_raw :: lid -> Id -> raw_symbol
         id_to_raw l :: lid
l _ = lid -> String -> raw_symbol
forall lid a. Language lid => lid -> String -> a
statError lid
l "id_to_raw"
         {- | Check whether a symbol matches a raw symbol, for
            example, f:s->t matches f. See CASL RefMan p. 192 -}
         matches :: lid -> symbol -> raw_symbol -> Bool
         matches _ _ _ = Bool
True

         -- ------------- operations on signatures and morphisms -----------

         -- | the empty (initial) signature, see CASL RefMan p. 193
         empty_signature :: lid -> sign
         -- | adds a symbol to a given signature
         add_symb_to_sign :: lid -> sign -> symbol -> Result sign
         add_symb_to_sign l :: lid
l _ _ = lid -> String -> Result sign
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "add_symb_to_sign"
         -- | union of signatures, see CASL RefMan p. 193
         signature_union :: lid -> sign -> sign -> Result sign
         signature_union l :: lid
l _ _ = lid -> String -> Result sign
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "signature_union"

         -- | difference of signatures resulting in unclosed pre-signatures
         signatureDiff :: lid -> sign -> sign -> Result sign
         signatureDiff l :: lid
l _ _ = lid -> String -> Result sign
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "signatureDiff"

         -- | intersection of signatures
         intersection :: lid -> sign -> sign -> Result sign
         intersection l :: lid
l _ _ = lid -> String -> Result sign
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "intersection"
         -- | final union of signatures, see CASL RefMan p. 194
         final_union :: lid -> sign -> sign -> Result sign
         final_union l :: lid
l _ _ = lid -> String -> Result sign
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "final_union"
         -- | union of signature morphims, see CASL RefMan p. 196
         morphism_union :: lid -> morphism -> morphism -> Result morphism
         morphism_union l :: lid
l _ _ = lid -> String -> Result morphism
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "morphism_union"
         -- | subsignatures, see CASL RefMan p. 194
         is_subsig :: lid -> sign -> sign -> Bool
         is_subsig _ _ _ = Bool
False
         {- | construct the inclusion morphisms between subsignatures,
              see CASL RefMan p. 194 -}
         subsig_inclusion :: lid -> sign -> sign -> Result morphism
         subsig_inclusion l :: lid
l _ _ = lid -> String -> Result morphism
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "subsig_inclusion"
         {- | the signature (co)generated by a set of symbols in another
            signature is the smallest (largest) signature containing
            (excluding) the set of symbols. Needed for revealing and
            hiding, see CASL RefMan p. 197ff. -}
         generated_sign, cogenerated_sign ::
             lid -> Set.Set symbol -> sign -> Result morphism
         generated_sign l :: lid
l _ _ = lid -> String -> Result morphism
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "generated_sign"
         cogenerated_sign l :: lid
l _ _ = lid -> String -> Result morphism
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "cogenerated_sign"
         {- | Induce a signature morphism from a source signature and
            a raw symbol map. Needed for translation (SP with SM).
            See CASL RefMan p. 198 -}
         induced_from_morphism ::
             lid -> EndoMap raw_symbol -> sign -> Result morphism
         induced_from_morphism l :: lid
l _ _ = lid -> String -> Result morphism
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "induced_from_morphism"
         {- | Induce a signature morphism between two signatures by a
            raw symbol map. Needed for instantiation and views.
            See CASL RefMan p. 198f. -}
         induced_from_to_morphism ::
             lid -> EndoMap raw_symbol -> ExtSign sign symbol
                 -> ExtSign sign symbol -> Result morphism
         induced_from_to_morphism l :: lid
l rm :: EndoMap raw_symbol
rm (ExtSign sig :: sign
sig _) (ExtSign tar :: sign
tar _) = do
           morphism
mor <- lid -> EndoMap raw_symbol -> sign -> Result morphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> EndoMap raw_symbol -> sign -> Result morphism
induced_from_morphism lid
l EndoMap raw_symbol
rm sign
sig
           lid -> sign -> sign -> Result morphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result morphism
inclusion lid
l (morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
mor) sign
tar Result morphism -> (morphism -> Result morphism) -> Result morphism
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= morphism -> morphism -> Result morphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
composeMorphisms morphism
mor
         {- | Check whether a signature morphism is transportable.
            See CASL RefMan p. 304f. -}
         is_transportable :: lid -> morphism -> Bool
         is_transportable _ _ = Bool
False
         {- | Check whether the underlying symbol map of a signature morphism
            is injective -}
         is_injective :: lid -> morphism -> Bool
         is_injective _ _ = Bool
False
         -- | generate an ontological taxonomy, if this makes sense
         theory_to_taxonomy :: lid
                            -> TaxoGraphKind
                            -> MMiSSOntology
                            -> sign -> [Named sentence]
                            -> Result MMiSSOntology
         theory_to_taxonomy l :: lid
l _ _ _ _ = lid -> String -> Result MMiSSOntology
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "theory_to_taxonomy"
         -- | create a theory from a correspondence
         corresp2th :: lid
                    -> String -- the name of the alignment
                    -> Bool   -- flag: should we disambiguate in the bridge
                    -> sign
                    -> sign
                    -> [symb_items]
                    -> [symb_items]
                    -> EndoMap symbol
                    -> EndoMap symbol
                    -> REL_REF
                    -> Result (sign, [Named sentence], sign, sign,
                               EndoMap symbol, EndoMap symbol)
         corresp2th _ _ _ _ _ _ _ _ _ = String
-> REL_REF
-> Result
     (sign, [Named sentence], sign, sign, EndoMap symbol,
      EndoMap symbol)
forall a. HasCallStack => String -> a
error "c2th nyi"
         -- | create a co-span fragment from an equivalence
         equiv2cospan :: lid -> sign -> sign -> [symb_items] -> [symb_items]
           -> Result (sign, sign, sign, EndoMap symbol, EndoMap symbol)
         equiv2cospan _ _ _ _ _ = String -> Result (sign, sign, sign, EndoMap symbol, EndoMap symbol)
forall a. HasCallStack => String -> a
error "equiv2cospan nyi"
         -- | extract the module
         extract_module :: lid -> [IRI] -> (sign, [Named sentence])
                        -> Result (sign, [Named sentence])
         extract_module _ _ = (sign, [Named sentence]) -> Result (sign, [Named sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return

-- | print a whole theory
printTheory :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items
               sign morphism symbol raw_symbol
  => Maybe IRI -> lid -> (sign, [Named sentence]) -> Doc
printTheory :: Maybe IRI -> lid -> (sign, [Named sentence]) -> Doc
printTheory sm :: Maybe IRI
sm lid :: lid
lid th :: (sign, [Named sentence])
th@(s :: sign
s, l :: [Named sentence]
l) = case
           (lid -> Maybe ((sign, [Named sentence]) -> basic_spec)
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> Maybe ((sign, [Named sentence]) -> basic_spec)
convertTheory lid
lid, Maybe IRI -> lid -> Maybe (basic_spec -> Doc)
forall lid basic_spec symbol symb_items symb_map_items.
Syntax lid basic_spec symbol symb_items symb_map_items =>
Maybe IRI -> lid -> Maybe (basic_spec -> Doc)
basicSpecPrinter Maybe IRI
sm lid
lid) of
             (Just c :: (sign, [Named sentence]) -> basic_spec
c, Just p :: basic_spec -> Doc
p) -> basic_spec -> Doc
p ((sign, [Named sentence]) -> basic_spec
c (sign, [Named sentence])
th)
             _ -> lid -> sign -> Doc
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Doc
print_sign lid
lid sign
s Doc -> Doc -> Doc
$++$ [Doc] -> Doc
vsep ((Named sentence -> Doc) -> [Named sentence] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (lid -> Named sentence -> Doc
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> Named sentence -> Doc
print_named lid
lid) [Named sentence]
l)

-- | guarded inclusion
inclusion :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items
             sign morphism symbol raw_symbol
          => lid -> sign -> sign -> Result morphism
inclusion :: lid -> sign -> sign -> Result morphism
inclusion l :: lid
l s1 :: sign
s1 s2 :: sign
s2 = if lid -> sign -> sign -> Bool
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Bool
is_subsig lid
l sign
s1 sign
s2 then lid -> sign -> sign -> Result morphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result morphism
subsig_inclusion lid
l sign
s1 sign
s2
  else String -> Result morphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result morphism) -> String -> Result morphism
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep
       [ String -> Doc
text (lid -> String
forall lid. Language lid => lid -> String
language_name lid
l)
       , String -> Doc
text "cannot construct inclusion. Symbol(s) missing in target:"
       , Set symbol -> Doc
forall a. Pretty a => a -> Doc
pretty (Set symbol -> Doc) -> Set symbol -> Doc
forall a b. (a -> b) -> a -> b
$ Set symbol -> Set symbol -> Set symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (lid -> sign -> Set symbol
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid
l sign
s1) (Set symbol -> Set symbol) -> Set symbol -> Set symbol
forall a b. (a -> b) -> a -> b
$ lid -> sign -> Set symbol
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid
l sign
s2
       , String -> Doc
text "\nSource is: "
       , Set symbol -> Doc
forall a. Pretty a => a -> Doc
pretty (Set symbol -> Doc) -> Set symbol -> Doc
forall a b. (a -> b) -> a -> b
$ lid -> sign -> Set symbol
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid
l sign
s1
       , String -> Doc
text "\nTarget is: "
       , Set symbol -> Doc
forall a. Pretty a => a -> Doc
pretty (Set symbol -> Doc) -> Set symbol -> Doc
forall a b. (a -> b) -> a -> b
$ lid -> sign -> Set symbol
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid
l sign
s2 ]

{- | semi lattices with top (needed for sublogics). Note that `Ord` is
only used for efficiency and is not related to the /partial/ order given
by the lattice. Only `Eq` is used to define `isSubElem` -}
class (Ord l, Show l) => SemiLatticeWithTop l where
  lub :: l -> l -> l -- least upper bound or "join"
  top :: l

instance SemiLatticeWithTop () where
  lub :: () -> () -> ()
lub _ _ = ()
  top :: ()
top = ()

-- | less or equal for semi lattices
isSubElem :: SemiLatticeWithTop l => l -> l -> Bool
isSubElem :: l -> l -> Bool
isSubElem a :: l
a b :: l
b = l -> l -> l
forall l. SemiLatticeWithTop l => l -> l -> l
lub l
a l
b l -> l -> Bool
forall a. Eq a => a -> a -> Bool
== l
b

-- | class providing the minimal sublogic of an item
class MinSublogic sublogic item where
    minSublogic :: item -> sublogic

-- | a default instance for no sublogics
instance MinSublogic () a where
    minSublogic :: a -> ()
minSublogic _ = ()

-- | class providing also the projection of an item to a sublogic
class MinSublogic sublogic item => ProjectSublogic sublogic item where
    projectSublogic :: sublogic -> item -> item

-- | a default instance for no sublogics
instance ProjectSublogic () b where
    projectSublogic :: () -> b -> b
projectSublogic _ = b -> b
forall a. a -> a
id

-- | like ProjectSublogic, but providing a partial projection
class MinSublogic sublogic item => ProjectSublogicM sublogic item where
    projectSublogicM :: sublogic -> item -> Maybe item

-- | a default instance for no sublogics
instance ProjectSublogicM () b where
    projectSublogicM :: () -> b -> Maybe b
projectSublogicM _ = b -> Maybe b
forall a. a -> Maybe a
Just

-- | a class for providing a sublogi name
class SublogicName l where
    sublogicName :: l -> String

instance SublogicName () where
    sublogicName :: () -> String
sublogicName () = ""

-- | a type for syntax information eventually stored in the signature
type SyntaxTable = (PrecMap, AssocMap)

{- Type class logic. The central type class of Hets, providing the
   interface for logics. This type class is instantiated for many logics,
   and it is used for the logic independent parts of Hets.
   It hence provides an abstraction barrier between logic specific and
   logic indepdendent code.
   This type class extends the class StaticAnalysis by a sublogic mechanism.
   Sublogics are important since they avoid the need to provide an own
   instance of the class logic for each sublogic. Instead, the sublogic
   can use the datastructures and operations of the main logic, and
   functions are provided to test whether a given item lies within the
   sublogic. Also, projection functions from a super-logic to a sublogic
   are provided.
-}
class (StaticAnalysis lid
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol,
       SemiLatticeWithTop sublogics,
       MinSublogic sublogics sentence,
       ProjectSublogic sublogics basic_spec,
       ProjectSublogicM sublogics symb_items,
       ProjectSublogicM sublogics symb_map_items,
       ProjectSublogic sublogics sign,
       ProjectSublogic sublogics morphism,
       ProjectSublogicM sublogics symbol,
       Convertible sublogics,
       SublogicName sublogics,
       Ord proof_tree, Show proof_tree,
       Convertible proof_tree)
    => Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree
        | lid -> sublogics
                 basic_spec sentence symb_items symb_map_items
                 sign morphism symbol raw_symbol proof_tree
          where
         -- Parser of sentence (Added for Hybridized logics)
         parse_basic_sen :: lid -> Maybe (basic_spec -> AParser st sentence)
         parse_basic_sen _ = Maybe (basic_spec -> AParser st sentence)
forall a. Maybe a
Nothing

         -- | stability of the implementation
         stability :: lid -> Stability
         stability _ = Stability
Experimental

         -- | for a process logic, return its data logic
         data_logic :: lid -> Maybe AnyLogic
         data_logic _ = Maybe AnyLogic
forall a. Maybe a
Nothing

         -- | the top sublogic, corresponding to the whole logic
         top_sublogic :: lid -> sublogics
         top_sublogic _ = sublogics
forall l. SemiLatticeWithTop l => l
top

         -- | list all the sublogics of the current logic
         all_sublogics :: lid -> [sublogics]
         all_sublogics li :: lid
li = [lid -> sublogics
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics
top_sublogic lid
li]

         {- a bottom sublogic can be extended along several dimensions
         joining all last elements of a dimension should yield the top-sublogic
         -}
         bottomSublogic :: lid -> Maybe sublogics
         bottomSublogic _ = Maybe sublogics
forall a. Maybe a
Nothing

         sublogicDimensions :: lid -> [[sublogics]]
         sublogicDimensions li :: lid
li = [lid -> [sublogics]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [sublogics]
all_sublogics lid
li]

         -- | parse sublogic (override more efficiently)
         parseSublogic :: lid -> String -> Maybe sublogics
         parseSublogic li :: lid
li s :: String
s = String -> [(String, sublogics)] -> Maybe sublogics
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
s ([(String, sublogics)] -> Maybe sublogics)
-> [(String, sublogics)] -> Maybe sublogics
forall a b. (a -> b) -> a -> b
$ (sublogics -> (String, sublogics))
-> [sublogics] -> [(String, sublogics)]
forall a b. (a -> b) -> [a] -> [b]
map (\ l :: sublogics
l -> (sublogics -> String
forall l. SublogicName l => l -> String
sublogicName sublogics
l, sublogics
l))
           ([sublogics] -> [(String, sublogics)])
-> [sublogics] -> [(String, sublogics)]
forall a b. (a -> b) -> a -> b
$ lid -> [sublogics]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [sublogics]
all_sublogics lid
li

         {- | provide the embedding of a projected signature into the
              original signature -}
         proj_sublogic_epsilon :: lid -> sublogics -> sign -> morphism
         proj_sublogic_epsilon _ _ = sign -> morphism
forall object morphism.
Category object morphism =>
object -> morphism
ide

         -- --------------------- provers ---------------------------

         -- | several provers can be provided. See module "Logic.Prover"
         provers :: lid -> [Prover sign sentence morphism sublogics proof_tree]
         provers _ = []

         -- | name of default prover, empty if none available
         default_prover :: lid -> String
         default_prover _ = ""
         
         -- | consistency checkers
         cons_checkers :: lid
                       -> [ConsChecker sign sentence
                                       sublogics morphism proof_tree]
         cons_checkers _ = []
         -- | conservativity checkers
         conservativityCheck :: lid
                             -> [ConservativityChecker sign sentence morphism]
         conservativityCheck _ = []
         -- | the empty proof tree
         empty_proof_tree :: lid -> proof_tree
         empty_proof_tree l :: lid
l = lid -> String -> proof_tree
forall lid a. Language lid => lid -> String -> a
statError lid
l "empty_proof_tree"

         -- --------------------- OMDoc ---------------------------

         syntaxTable :: lid -> sign -> Maybe SyntaxTable
         syntaxTable _ _ = Maybe SyntaxTable
forall a. Maybe a
Nothing

         omdoc_metatheory :: lid -> Maybe OMDoc.OMCD
         {- default implementation, no logic should throw an error here
         and the base of omcd should be a parseable URI -}
         omdoc_metatheory _ = Maybe OMCD
forall a. Maybe a
Nothing


         export_symToOmdoc :: lid -> OMDoc.NameMap symbol
                           -> symbol -> String -> Result OMDoc.TCElement
         export_symToOmdoc l :: lid
l _ _ _ = lid -> String -> Result TCElement
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "export_symToOmdoc"

         export_senToOmdoc :: lid -> OMDoc.NameMap symbol
                          -> sentence -> Result OMDoc.TCorOMElement
         export_senToOmdoc l :: lid
l _ _ = lid -> String -> Result TCorOMElement
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "export_senToOmdoc"

         {- | additional information which has to be exported can be
         exported by this function -}
         export_theoryToOmdoc :: lid -> OMDoc.SigMap symbol -> sign
                              -> [Named sentence] -> Result [OMDoc.TCElement]
         {- default implementation does no extra export
         , sufficient in some cases -}
         export_theoryToOmdoc _ _ _ _ = [TCElement] -> Result [TCElement]
forall (m :: * -> *) a. Monad m => a -> m a
return []


         omdocToSym :: lid -> OMDoc.SigMapI symbol -> OMDoc.TCElement
                    -> String -> Result symbol
         omdocToSym l :: lid
l _ _ _ = lid -> String -> Result symbol
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "omdocToSym"

         omdocToSen :: lid -> OMDoc.SigMapI symbol -> OMDoc.TCElement
                    -> String -> Result (Maybe (Named sentence))
         omdocToSen l :: lid
l _ _ _ = lid -> String -> Result (Maybe (Named sentence))
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail lid
l "omdocToSen"

         {- | Algebraic Data Types are imported with this function.
         By default the input is returned without changes. -}
         addOMadtToTheory :: lid -> OMDoc.SigMapI symbol
                          -> (sign, [Named sentence]) -> [[OMDoc.OmdADT]]
                          -> Result (sign, [Named sentence])
         -- no logic should throw an error here
         addOMadtToTheory l :: lid
l _ t :: (sign, [Named sentence])
t adts :: [[OmdADT]]
adts = do
           Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([[OmdADT]] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[OmdADT]]
adts) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
warning ()
                      ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ "ADT handling not implemented for logic "
                              , lid -> String
forall a. Show a => a -> String
show lid
l, " but some adts have to be handled" ])
                      Range
nullRange
           (sign, [Named sentence]) -> Result (sign, [Named sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (sign, [Named sentence])
t

         {- | additional information which has to be imported can be
         imported by this function. By default the input is returned
         without changes. -}
         addOmdocToTheory :: lid -> OMDoc.SigMapI symbol
                          -> (sign, [Named sentence]) -> [OMDoc.TCElement]
                          -> Result (sign, [Named sentence])
         -- no logic should throw an error here
         addOmdocToTheory _ _ t :: (sign, [Named sentence])
t _ = (sign, [Named sentence]) -> Result (sign, [Named sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (sign, [Named sentence])
t

         -- | sublogic of a theory
         sublogicOfTheo :: lid -> (sign, [sentence]) -> sublogics
         sublogicOfTheo _ (sig :: sign
sig, axs :: [sentence]
axs) = 
            (sublogics -> sublogics -> sublogics)
-> sublogics -> [sublogics] -> sublogics
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl sublogics -> sublogics -> sublogics
forall l. SemiLatticeWithTop l => l -> l -> l
lub (sign -> sublogics
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic sign
sig) ([sublogics] -> sublogics) -> [sublogics] -> sublogics
forall a b. (a -> b) -> a -> b
$ (sentence -> sublogics) -> [sentence] -> [sublogics]
forall a b. (a -> b) -> [a] -> [b]
map sentence -> sublogics
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic [sentence]
axs




{- The class of logics which can be used as logical frameworks, in which object
   logics can be specified by the user. Currently the only logics implementing
   this class are LF, Maude, and Isabelle, with the latter two only having
   dummy implementations.

   The function "base_sig" returns the base signature of the framework -
   for details see Integrating Logical Frameworks in Hets by M. Codescu et al
   (WADT10).

   The function "write_logic" constructs the contents of the Logic_L
   file, where L is the name of the object logic passed as an argument.
   Typically, this file will declare the lid of the object logic L and
   instances of the classes Language, Syntax, Sentences, Logic, and
   StaticAnalysis. The instance of Category is usually inherited from
   the framework itself as the object logic reuses the signatures and
   morphisms of the framework.

   The function "write_syntax" constructs the contents of the file declaring
   the Ltruth morphism (see the reference given above). If proofs and models
   are later integrated into Hets, there should be analogous functions
   "write_proofs" and "write_models" added, declaring the Lpf and
   Lmod morphisms respectively. -}
class Logic lid sublogics basic_spec sentence
            symb_items symb_map_items sign
            morphism symbol raw_symbol proof_tree
      => LogicalFramework lid sublogics basic_spec sentence
            symb_items symb_map_items sign
            morphism symbol raw_symbol proof_tree
            | lid -> sublogics basic_spec sentence symb_items symb_map_items
                     sign morphism symbol raw_symbol proof_tree
      where
      -- | the base signature
      base_sig :: lid -> sign
      base_sig l :: lid
l = String -> sign
forall a. HasCallStack => String -> a
error (String -> sign) -> String -> sign
forall a b. (a -> b) -> a -> b
$ "Function base_sig nyi for logic " String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid -> ShowS
forall a. Show a => a -> ShowS
shows lid
l "."

      {- | generation of the object logic instances
           second argument is object logic name -}
      write_logic :: lid -> String -> String
      write_logic l :: lid
l = String -> ShowS
forall a. HasCallStack => String -> a
error
         (String -> ShowS) -> String -> ShowS
forall a b. (a -> b) -> a -> b
$ "Function write_logic nyi for logic " String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid -> ShowS
forall a. Show a => a -> ShowS
shows lid
l "."

      {- | generation of the Ltruth morphism declaration
           second argument is the object logic name
           third argument is the Ltruth morphism -}
      write_syntax :: lid -> String -> morphism -> String
      write_syntax l :: lid
l = String -> String -> morphism -> String
forall a. HasCallStack => String -> a
error (String -> String -> morphism -> String)
-> String -> String -> morphism -> String
forall a b. (a -> b) -> a -> b
$
         "Function write_syntax nyi for logic " String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid -> ShowS
forall a. Show a => a -> ShowS
shows lid
l "."
      write_proof :: lid -> String -> morphism -> String
      write_proof l :: lid
l = String -> String -> morphism -> String
forall a. HasCallStack => String -> a
error (String -> String -> morphism -> String)
-> String -> String -> morphism -> String
forall a b. (a -> b) -> a -> b
$
         "Function write_proof nyi for logic " String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid -> ShowS
forall a. Show a => a -> ShowS
shows lid
l "."
      write_model :: lid -> String -> morphism -> String
      write_model l :: lid
l = String -> String -> morphism -> String
forall a. HasCallStack => String -> a
error (String -> String -> morphism -> String)
-> String -> String -> morphism -> String
forall a b. (a -> b) -> a -> b
$
         "Function write_model nyi for logic " String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid -> ShowS
forall a. Show a => a -> ShowS
shows lid
l "."
      read_morphism :: lid -> FilePath -> morphism
      read_morphism l :: lid
l _ = String -> morphism
forall a. HasCallStack => String -> a
error (String -> morphism) -> String -> morphism
forall a b. (a -> b) -> a -> b
$
         "Function read_morphism nyi for logic " String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid -> ShowS
forall a. Show a => a -> ShowS
shows lid
l "."

      write_comorphism :: lid -> String -> String -> String
                           -> morphism -> morphism -> morphism
                           -> String
      write_comorphism l :: lid
l = String
-> String
-> String
-> String
-> morphism
-> morphism
-> morphism
-> String
forall a. HasCallStack => String -> a
error (String
 -> String
 -> String
 -> String
 -> morphism
 -> morphism
 -> morphism
 -> String)
-> String
-> String
-> String
-> String
-> morphism
-> morphism
-> morphism
-> String
forall a b. (a -> b) -> a -> b
$
         "Function write_comorphism nyi for logic " String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid -> ShowS
forall a. Show a => a -> ShowS
shows lid
l "."

{- --------------------------------------------------------------
Derived functions
-------------------------------------------------------------- -}

-- | the empty theory
emptyTheory :: StaticAnalysis lid
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol =>
        lid -> Theory sign sentence proof_tree
emptyTheory :: lid -> Theory sign sentence proof_tree
emptyTheory lid :: lid
lid = sign
-> ThSens sentence (ProofStatus proof_tree)
-> Theory sign sentence proof_tree
forall sign sen proof_tree.
sign
-> ThSens sen (ProofStatus proof_tree)
-> Theory sign sen proof_tree
Theory (lid -> sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign
empty_signature lid
lid) ThSens sentence (ProofStatus proof_tree)
forall k a. Map k a
Map.empty

{- --------------------------------------------------------------
Existential type covering any logic
-------------------------------------------------------------- -}

-- | the disjoint union of all logics
data AnyLogic = forall lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree .
        Logic lid sublogics
         basic_spec sentence symb_items symb_map_items
         sign morphism symbol raw_symbol proof_tree =>
        Logic lid
  deriving Typeable

instance GetRange AnyLogic

instance Show AnyLogic where
  show :: AnyLogic -> String
show (Logic lid :: lid
lid) = lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid

instance Eq AnyLogic where
  a :: AnyLogic
a == :: AnyLogic -> AnyLogic -> Bool
== b :: AnyLogic
b = AnyLogic -> AnyLogic -> Ordering
forall a. Ord a => a -> a -> Ordering
compare AnyLogic
a AnyLogic
b Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance Ord AnyLogic where
  compare :: AnyLogic -> AnyLogic -> Ordering
compare = (AnyLogic -> String) -> AnyLogic -> AnyLogic -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing AnyLogic -> String
forall a. Show a => a -> String
show

{- class hierarchy:
                            Language
               __________/
   Category
      |                  /
   Sentences      Syntax
      \            /
      StaticAnalysis (no sublogics)
            |
            |
           Logic
-}