{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Framework/Logic_Framework.hs
Description :  Instances of Logic and other classes for the logic Framework
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  k.sojakova@jacobs-university.de
Stability   :  experimental
Portability :  portable

  Signatures of this logic are composed of a logical framework name
    (currently one of LF, Isabelle, or Maude) to be used as a meta-logic,
    and a tuple of signature and morphism names which determine
    the object logic. As such the logic Framework does not have any
    sentences and only identity signature morphisms.

  For reference see Integrating Logical Frameworks in Hets by M. Codescu et al
    (WADT10).
-}

module Framework.Logic_Framework where

import Framework.AS
import Framework.ATC_Framework ()

import Logic.Logic

import Data.Monoid ()

import Common.DefaultMorphism

type Morphism = DefaultMorphism LogicDef

-- lid for logical frameworks
data Framework = Framework deriving Int -> Framework -> ShowS
[Framework] -> ShowS
Framework -> String
(Int -> Framework -> ShowS)
-> (Framework -> String)
-> ([Framework] -> ShowS)
-> Show Framework
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Framework] -> ShowS
$cshowList :: [Framework] -> ShowS
show :: Framework -> String
$cshow :: Framework -> String
showsPrec :: Int -> Framework -> ShowS
$cshowsPrec :: Int -> Framework -> ShowS
Show

instance Language Framework where
   description :: Framework -> String
description _ = "A framework allowing to add logics dynamically."

instance Semigroup LogicDef where
   _ <> :: LogicDef -> LogicDef -> LogicDef
<> _ = LogicDef
forall a. Monoid a => a
mempty
instance Monoid LogicDef where
   mempty :: LogicDef
mempty = String -> LogicDef
forall a. HasCallStack => String -> a
error "Framework.Logic_Framework: Monoid LogicDef"

-- syntax for Framework
instance Syntax Framework LogicDef () () ()

-- sentences for Framework
instance Sentences Framework () LogicDef Morphism ()

-- static analysis for Framework
instance StaticAnalysis Framework LogicDef () () ()
         LogicDef Morphism () () where
  empty_signature :: Framework -> LogicDef
empty_signature Framework = String -> LogicDef
forall a. HasCallStack => String -> a
error
       "Logic Framework does not have an empty signature."

-- instance of logic for Framework
instance Logic Framework () LogicDef () () () LogicDef Morphism () () ()


{- ------------------------------------------------------------------------------
FrameworkCom -     logical framework for the analysis of comorphisms -}
type MorphismCom = DefaultMorphism ComorphismDef

data FrameworkCom = FrameworkCom deriving Int -> FrameworkCom -> ShowS
[FrameworkCom] -> ShowS
FrameworkCom -> String
(Int -> FrameworkCom -> ShowS)
-> (FrameworkCom -> String)
-> ([FrameworkCom] -> ShowS)
-> Show FrameworkCom
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FrameworkCom] -> ShowS
$cshowList :: [FrameworkCom] -> ShowS
show :: FrameworkCom -> String
$cshow :: FrameworkCom -> String
showsPrec :: Int -> FrameworkCom -> ShowS
$cshowsPrec :: Int -> FrameworkCom -> ShowS
Show

instance Language FrameworkCom where
   description :: FrameworkCom -> String
description _ = "A framework allowing to add comorphisms between " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                   "logics dynamically."

instance Semigroup ComorphismDef where
   _ <> :: ComorphismDef -> ComorphismDef -> ComorphismDef
<> _ = ComorphismDef
forall a. Monoid a => a
mempty
instance Monoid ComorphismDef where
   mempty :: ComorphismDef
mempty = String -> ComorphismDef
forall a. HasCallStack => String -> a
error "Framework.Logic_Framework Monoid ComorphismDef"

-- syntax for Framework
instance Syntax FrameworkCom ComorphismDef () () ()

-- sentences for Framework
instance Sentences FrameworkCom () ComorphismDef MorphismCom ()

-- static analysis for Framework
instance StaticAnalysis FrameworkCom ComorphismDef () () ()
         ComorphismDef MorphismCom () () where
  empty_signature :: FrameworkCom -> ComorphismDef
empty_signature FrameworkCom = String -> ComorphismDef
forall a. HasCallStack => String -> a
error
       "Logic FrameworkCom does not have an empty signature."

-- instance of logic for Framework
instance Logic FrameworkCom () ComorphismDef () () () ComorphismDef
         MorphismCom () () ()