{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  $Header$
Description :  Abstract syntax for logic definitions
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt

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

module Framework.AS where

import Common.Id
import Common.IRI (IRI)
import Common.Doc
import Common.DocUtils
import Common.Keywords

import Data.Data

type NAME = IRI
type SIG_NAME = IRI
type MORPH_NAME = IRI
type PATTERN_NAME = Token

data FRAM = LF | Isabelle | Maude deriving (Show, Eq, Ord, Typeable, Data)

data LogicDef = LogicDef
  { -- the name of the object logic
    newlogicName :: NAME,
    -- the framework used for defining the object logic
    meta :: FRAM,
    {- name of the morphism specifying the sentences and truth judgement of the
       object logic -}
    syntax :: MORPH_NAME,
    -- name of the morphism specifying the model category of the object logic
    models :: MORPH_NAME,
    -- the foundation used to construct the model theory of the object logic
    foundation :: SIG_NAME,
    -- name of the morphism specifying the proof category of the object logic
    proofs :: MORPH_NAME,
    -- name of the pattern specifying the signature category of the object logic
    patterns :: PATTERN_NAME
  } deriving (Show, Eq, Ord, Typeable, Data)

data ComorphismDef = ComorphismDef
  { -- the name of the comorphism
    newcomorphismName :: NAME,
    -- the framework used for defining the comorphism
    metaC :: FRAM,
    -- name of the source logic
    source :: SIG_NAME,
    -- name of the target logic
    target :: SIG_NAME,
    {- name of the morphism between the syntax of the source logic and
       the syntax of the target logic -}
    syntaxC :: MORPH_NAME,
    {- name of the morphism between the model category of the source logic and
       the model category of the target logic -}
    modelC :: MORPH_NAME,
    {- name of the morphism between the proof category of the source logic and
       the proof category of the target logic -}
    proofC :: MORPH_NAME
  } deriving (Show, Eq, Ord, Typeable, Data)

instance GetRange LogicDef
instance GetRange ComorphismDef

instance Pretty LogicDef where
    pretty = printLogicDef
instance Pretty ComorphismDef where
    pretty = printComorphismDef
instance Pretty FRAM where
    pretty = printFram

printLogicDef :: LogicDef -> Doc
printLogicDef (LogicDef l ml s m f p pa) =
  vcat [ text newlogicS <+> pretty l
       , text " " <+> text metaS <+> pretty ml
       , text " " <+> text syntaxS <+> pretty s
       , text " " <+> text modelsS <+> pretty m
       , text " " <+> text foundationS <+> pretty f
       , text " " <+> text proofsS <+> pretty p
       , text " " <+> text patternsS <+> pretty pa
       ]

printComorphismDef :: ComorphismDef -> Doc
printComorphismDef (ComorphismDef c ml sl tl s m p) =
  vcat [ text newcomorphismS <+> pretty c
       , text " " <+> text metaS <+> pretty ml
       , text " " <+> text sourceS <+> pretty sl
       , text " " <+> text targetS <+> pretty tl
       , text " " <+> text syntaxS <+> pretty s
       , text " " <+> text modelsS <+> pretty m
       , text " " <+> text proofsS <+> pretty p
       ]

printFram :: FRAM -> Doc
printFram LF = text "LF"
printFram Isabelle = text "Isabelle"
printFram Maude = text "Maude"
