{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-}
{- |
Module      :  ./QVTR/Logic_QVTR.hs
Description :  Instance of class Logic for the QVTR 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 QVTR.Logic_QVTR where

import QVTR.As
import QVTR.Sign
import QVTR.Print ()
import QVTR.StatAna

import QVTR.ATC_QVTR ()

import Logic.Logic

import Common.DefaultMorphism

import Data.Monoid ()

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

instance Language QVTR where
  description :: QVTR -> String
description _ = "OMG's QVT-Relations transformation, a language for the specification of model transformations"

type Morphism = DefaultMorphism Sign


-- QVTR logic

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

instance Sentences QVTR
  Sen
  Sign
  Morphism
  ()
  where
    map_sen :: QVTR -> Morphism -> Sen -> Result Sen
map_sen QVTR _ = Sen -> Result Sen
forall (m :: * -> *) a. Monad m => a -> m a
return


instance Syntax QVTR
  Transformation
  ()
  ()
  ()


instance Logic QVTR
  ()                -- Sublogics
  Transformation    -- basic_spec
  Sen               -- sentence
  ()                -- symb_items
  ()                -- symb_map_items
  Sign              -- sign
  Morphism          -- morphism
  ()                -- symbol
  ()                -- raw_symbol
  ()                -- proof_tree
  where
    stability :: QVTR -> Stability
stability QVTR = Stability
Experimental
    empty_proof_tree :: QVTR -> ()
empty_proof_tree _ = ()


instance StaticAnalysis QVTR
  Transformation    -- basic_spec
  Sen               -- sentence
  ()                -- symb_items
  ()                -- symb_map_items
  Sign              -- sign
  Morphism          -- morphism
  ()                -- symbol
  ()                -- raw_symbol
  where
    basic_analysis :: QVTR
-> Maybe
     ((Transformation, Sign, GlobalAnnos)
      -> Result (Transformation, ExtSign Sign (), [Named Sen]))
basic_analysis QVTR = ((Transformation, Sign, GlobalAnnos)
 -> Result (Transformation, ExtSign Sign (), [Named Sen]))
-> Maybe
     ((Transformation, Sign, GlobalAnnos)
      -> Result (Transformation, ExtSign Sign (), [Named Sen]))
forall a. a -> Maybe a
Just (Transformation, Sign, GlobalAnnos)
-> Result (Transformation, ExtSign Sign (), [Named Sen])
basicAna
    empty_signature :: QVTR -> Sign
empty_signature QVTR = Sign
emptySign
    is_subsig :: QVTR -> Sign -> Sign -> Bool
is_subsig QVTR _ _ = Bool
True
    subsig_inclusion :: QVTR -> Sign -> Sign -> Result Morphism
subsig_inclusion QVTR = Sign -> Sign -> Result Morphism
forall (m :: * -> *) sign.
Monad m =>
sign -> sign -> m (DefaultMorphism sign)
defaultInclusion
    induced_from_morphism :: QVTR -> 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 :: QVTR -> Sign -> Sign -> Result Sign
signature_union QVTR sign1 :: Sign
sign1 _ = Sign -> Result Sign
forall (m :: * -> *) a. Monad m => a -> m a
return Sign
sign1 -- TODO