content: {-# LANGUAGE DeriveDataTypeable #-}
  {- |
  Module      :  ./Framework/AS.hs
  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"
  