Logic_CSMOF.hs

{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-}
{- |
Module      :  ./CSMOF/Logic_CSMOF.hs
Description :  Instance of class Logic for the CSMOF logic
Copyright   :  (c) Daniel Calegari Universidad de la Republica, Uruguay 2013
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  dcalegar@fing.edu.uy
Stability   :  provisional
Portability :  portable
-}

module CSMOF.Logic_CSMOF where

import CSMOF.As
import CSMOF.Sign
import CSMOF.Print ()
import CSMOF.StatAna
import CSMOF.ATC_CSMOF ()

import Logic.Logic

import Common.DefaultMorphism

import Data.Monoid ()

data CSMOF = CSMOF deriving Show

instance Language CSMOF where
  description _ = "OMG's meta-object facility, a language for the specification of metamodels"

type Morphism = DefaultMorphism Sign


-- CSMOF logic

instance Semigroup Metamodel where
  _ <> _ = error "Not implemented!"
instance Monoid Metamodel where
  mempty = error "Not implemented!"

instance Sentences CSMOF
  Sen
  Sign
  Morphism
  ()
  where
    map_sen CSMOF _ = return


instance Syntax CSMOF
  Metamodel
  ()
  ()
  ()


instance Logic CSMOF
  ()                -- Sublogics
  Metamodel         -- basic_spec
  Sen               -- sentence
  ()                -- symb_items
  ()                -- symb_map_items
  Sign              -- sign
  Morphism          -- morphism
  ()                -- symbol
  ()                -- raw_symbol
  ()                -- proof_tree
  where
    stability CSMOF = Experimental
    empty_proof_tree _ = ()


instance StaticAnalysis CSMOF
  Metamodel         -- basic_spec
  Sen               -- sentence
  ()                -- symb_items
  ()                -- symb_map_items
  Sign              -- sign
  Morphism          -- morphism
  ()                -- symbol
  ()                -- raw_symbol
  where
    basic_analysis CSMOF = Just basicAna
    empty_signature CSMOF = emptySign
    is_subsig CSMOF _ _ = True
    subsig_inclusion CSMOF = defaultInclusion
    induced_from_morphism _ _ sig = return $ MkMorphism sig sig
    signature_union CSMOF sign1 _ = return sign1 -- TODO