{-# 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 Int -> CSMOF -> ShowS
[CSMOF] -> ShowS
CSMOF -> String
(Int -> CSMOF -> ShowS)
-> (CSMOF -> String) -> ([CSMOF] -> ShowS) -> Show CSMOF
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CSMOF] -> ShowS
$cshowList :: [CSMOF] -> ShowS
show :: CSMOF -> String
$cshow :: CSMOF -> String
showsPrec :: Int -> CSMOF -> ShowS
$cshowsPrec :: Int -> CSMOF -> ShowS
Show

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

type Morphism = DefaultMorphism Sign


-- CSMOF logic

instance Semigroup Metamodel where
  _ <> :: Metamodel -> Metamodel -> Metamodel
<> _ = String -> Metamodel
forall a. HasCallStack => String -> a
error "Not implemented!"
instance Monoid Metamodel where
  mempty :: Metamodel
mempty = String -> Metamodel
forall a. HasCallStack => String -> a
error "Not implemented!"

instance Sentences CSMOF
  Sen
  Sign
  Morphism
  ()
  where
    map_sen :: CSMOF -> Morphism -> Sen -> Result Sen
map_sen CSMOF _ = Sen -> Result Sen
forall (m :: * -> *) a. Monad m => a -> m a
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 -> Stability
stability CSMOF = Stability
Experimental
    empty_proof_tree :: CSMOF -> ()
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
-> Maybe
     ((Metamodel, Sign, GlobalAnnos)
      -> Result (Metamodel, ExtSign Sign (), [Named Sen]))
basic_analysis CSMOF = ((Metamodel, Sign, GlobalAnnos)
 -> Result (Metamodel, ExtSign Sign (), [Named Sen]))
-> Maybe
     ((Metamodel, Sign, GlobalAnnos)
      -> Result (Metamodel, ExtSign Sign (), [Named Sen]))
forall a. a -> Maybe a
Just (Metamodel, Sign, GlobalAnnos)
-> Result (Metamodel, ExtSign Sign (), [Named Sen])
basicAna
    empty_signature :: CSMOF -> Sign
empty_signature CSMOF = Sign
emptySign
    is_subsig :: CSMOF -> Sign -> Sign -> Bool
is_subsig CSMOF _ _ = Bool
True
    subsig_inclusion :: CSMOF -> Sign -> Sign -> Result Morphism
subsig_inclusion CSMOF = Sign -> Sign -> Result Morphism
forall (m :: * -> *) sign.
Monad m =>
sign -> sign -> m (DefaultMorphism sign)
defaultInclusion
    induced_from_morphism :: CSMOF -> EndoMap () -> Sign -> Result Morphism
induced_from_morphism _ _ sig :: Sign
sig = Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism) -> Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$ Sign -> Sign -> Morphism
forall sign. sign -> sign -> DefaultMorphism sign
MkMorphism Sign
sig Sign
sig
    signature_union :: CSMOF -> Sign -> Sign -> Result Sign
signature_union CSMOF sign1 :: Sign
sign1 _ = Sign -> Result Sign
forall (m :: * -> *) a. Monad m => a -> m a
return Sign
sign1 -- TODO