{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./ConstraintCASL/Logic_ConstraintCASL.hs
Description :  instance of the class Logic for ConstraintCASL
Copyright   :  (c) Uni Bremen 2002-2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Here is the place where the class Logic is instantiated for CASL.
   Also the instances for Syntax an Category.
-}

module ConstraintCASL.Logic_ConstraintCASL where

import Logic.Logic

import ConstraintCASL.AS_ConstraintCASL
import ConstraintCASL.Formula
import ConstraintCASL.StaticAna
import ConstraintCASL.ATC_ConstraintCASL ()
import ConstraintCASL.Print_AS ()

import CASL.AS_Basic_CASL
import CASL.Parse_AS_Basic
import CASL.ToDoc ()
import CASL.SymbolParser
import CASL.MapSentence
import CASL.ATC_CASL ()
import CASL.Sublogic
import CASL.Sign
import CASL.Morphism
import CASL.SymbolMapAnalysis
import CASL.Logic_CASL

data ConstraintCASL = ConstraintCASL deriving Show

instance Language ConstraintCASL where
 description _ =
  "ConstraintCASL - a restriction of CASL to constraint "
  ++ "formulas over predicates"

instance Syntax ConstraintCASL ConstraintCASLBasicSpec
                Symbol SYMB_ITEMS SYMB_MAP_ITEMS
      where
         parse_basic_spec ConstraintCASL = Just $ basicSpec constraintKeywords
         parse_symb_items ConstraintCASL = Just $ symbItems []
         parse_symb_map_items ConstraintCASL = Just $ symbMapItems []

-- lattices (for sublogics) is missing

instance Sentences ConstraintCASL ConstraintCASLFORMULA
                   ConstraintCASLSign ConstraintCASLMor Symbol where
      map_sen ConstraintCASL m = return . mapSen (const id) m
      sym_of ConstraintCASL = symOf
      symmap_of ConstraintCASL = morphismToSymbMap
      sym_name ConstraintCASL = symName

instance StaticAnalysis ConstraintCASL
               ConstraintCASLBasicSpec ConstraintCASLFORMULA
               SYMB_ITEMS SYMB_MAP_ITEMS
               ConstraintCASLSign
               ConstraintCASLMor
               Symbol RawSymbol where
         basic_analysis ConstraintCASL = Just basicConstraintCASLAnalysis
         stat_symb_map_items ConstraintCASL = statSymbMapItems
         stat_symb_items ConstraintCASL = statSymbItems

         symbol_to_raw ConstraintCASL = symbolToRaw
         id_to_raw ConstraintCASL = idToRaw
         matches ConstraintCASL = CASL.Morphism.matches
         is_transportable ConstraintCASL = isSortInjective

         empty_signature ConstraintCASL = emptySign ()
         signature_union ConstraintCASL s = return . addSig const s
         morphism_union ConstraintCASL = plainMorphismUnion const
         final_union ConstraintCASL = finalUnion const
         is_subsig ConstraintCASL = isSubSig trueC
         subsig_inclusion ConstraintCASL = sigInclusion ()
         cogenerated_sign ConstraintCASL = cogeneratedSign ()
         generated_sign ConstraintCASL = generatedSign ()
         induced_from_morphism ConstraintCASL = inducedFromMorphism ()
         induced_from_to_morphism ConstraintCASL =
             inducedFromToMorphism () trueC const

instance MinSL () ConstraintFORMULA where
    minSL _ = bottom

instance ProjForm () ConstraintFORMULA where
    projForm _ = Just . ExtFORMULA

instance Logic ConstraintCASL CASL_Sublogics
               ConstraintCASLBasicSpec ConstraintCASLFORMULA
               SYMB_ITEMS SYMB_MAP_ITEMS
               ConstraintCASLSign
               ConstraintCASLMor
               Symbol RawSymbol () where

         stability _ = Experimental
         proj_sublogic_epsilon ConstraintCASL = pr_epsilon ()
         all_sublogics _ = sublogics_all [()]
         empty_proof_tree _ = ()
