{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
{- |
Module      :  ./CSL/Logic_CSL.hs
Description :  Instance of class Logic for CSL
Copyright   :  (c) Dominik Dietrich, DFKI Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  dominik.dietrich@dfki.de
Stability   :  experimental
Portability :  non-portable (imports Logic.Logic)

Instance of class Logic for the CSL logic
   Also the instances for Syntax and Category.

see
Dominik Dietrich, Lutz Schröder, and Ewaryst Schulz:
Formalizing and Operationalizing Industrial Standards.
D. Giannakopoulou and F. Orejas (Eds.): FASE 2011, LNCS 6603, pp. 81–95, 2011.
-}


module CSL.Logic_CSL where

import ATC.ProofTree ()

import CSL.AS_BASIC_CSL
import CSL.ATC_CSL ()
import CSL.Analysis
import CSL.Morphism
import CSL.Parse_AS_Basic
import CSL.ReduceProve
import CSL.Sign
import CSL.Symbol
import CSL.Tools

import qualified Data.Map as Map
import Data.Monoid ()

import Logic.Logic

-- | Lid for reduce logic
data CSL = CSL

instance Show CSL where
    show :: CSL -> String
show _ = "EnCL"

instance Language CSL where
    description :: CSL -> String
description _ = "A Domain-Specific Language for Engineering Calculations\n"
-- language_name _ = "EnCL"

-- | Instance of Category for CSL logic
instance Category Sign Morphism where
    -- Identity morhpism
    ide :: Sign -> Morphism
ide = Sign -> Morphism
idMor
    -- Returns the domain of a morphism
    dom :: Morphism -> Sign
dom = Morphism -> Sign
source
    -- Returns the codomain of a morphism
    cod :: Morphism -> Sign
cod = Morphism -> Sign
target
    -- check if morphism is inclusion
    isInclusion :: Morphism -> Bool
isInclusion = Map Id Id -> Bool
forall k a. Map k a -> Bool
Map.null (Map Id Id -> Bool) -> (Morphism -> Map Id Id) -> Morphism -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Map Id Id
operatorMap
    -- composition of morphisms
    composeMorphisms :: Morphism -> Morphism -> Result Morphism
composeMorphisms = Morphism -> Morphism -> Result Morphism
composeMor

-- | Instance of Sentences for reduce logic
instance Sentences CSL CMD
    Sign Morphism Symbol where
    negation :: CSL -> CMD -> Maybe CMD
negation CSL = CMD -> Maybe CMD
forall a. a -> Maybe a
Just (CMD -> Maybe CMD) -> (CMD -> CMD) -> CMD -> Maybe CMD
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CMD -> CMD
negateFormula
    -- returns the set of symbols --> including operators
    sym_of :: CSL -> Sign -> [Set Symbol]
sym_of CSL = Set Symbol -> [Set Symbol]
forall a. a -> [a]
singletonList (Set Symbol -> [Set Symbol])
-> (Sign -> Set Symbol) -> Sign -> [Set Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Set Symbol
symOf
    {- returns the symbol map -->
    the internal map only contains changes but the external symbol map
    must also contain identity mappings for all remaining symbols -}
    symmap_of :: CSL -> Morphism -> EndoMap Symbol
symmap_of CSL = Morphism -> EndoMap Symbol
getSymbolMap
    -- returns the name of a symbol --> id
    sym_name :: CSL -> Symbol -> Id
sym_name CSL = Symbol -> Id
getSymbolName
    {- translation of sentences along signature morphism -->
    rename the used operators according to the morphism -}
    map_sen :: CSL -> Morphism -> CMD -> Result CMD
map_sen CSL = Morphism -> CMD -> Result CMD
mapSentence
    -- there is nothing to leave out
    simplify_sen :: CSL -> Sign -> CMD -> CMD
simplify_sen CSL _ = CMD -> CMD
forall a. a -> a
id
    symKind :: CSL -> Symbol -> String
symKind CSL _ = "op"

instance Semigroup BASIC_SPEC where
    (Basic_spec l1 :: [Annoted BASIC_ITEM]
l1) <> :: BASIC_SPEC -> BASIC_SPEC -> BASIC_SPEC
<> (Basic_spec l2 :: [Annoted BASIC_ITEM]
l2) = [Annoted BASIC_ITEM] -> BASIC_SPEC
Basic_spec ([Annoted BASIC_ITEM] -> BASIC_SPEC)
-> [Annoted BASIC_ITEM] -> BASIC_SPEC
forall a b. (a -> b) -> a -> b
$ [Annoted BASIC_ITEM]
l1 [Annoted BASIC_ITEM]
-> [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]
forall a. [a] -> [a] -> [a]
++ [Annoted BASIC_ITEM]
l2
instance Monoid BASIC_SPEC where
    mempty :: BASIC_SPEC
mempty = [Annoted BASIC_ITEM] -> BASIC_SPEC
Basic_spec []

-- | Syntax of CSL logic
instance Syntax CSL BASIC_SPEC Symbol
    SYMB_ITEMS SYMB_MAP_ITEMS where
         parse_basic_spec :: CSL -> Maybe (PrefixMap -> AParser st BASIC_SPEC)
parse_basic_spec CSL = Maybe (PrefixMap -> AParser st BASIC_SPEC)
forall st. Maybe (PrefixMap -> AParser st BASIC_SPEC)
parseBasicSpec
         parse_symb_items :: CSL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items CSL = (AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS)
-> Maybe (AParser st SYMB_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS
forall a b. a -> b -> a
const Maybe (AParser st SYMB_ITEMS)
forall st. Maybe (GenParser Char st SYMB_ITEMS)
parseSymbItems
         parse_symb_map_items :: CSL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items CSL = (AParser st SYMB_MAP_ITEMS
 -> PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> Maybe (AParser st SYMB_MAP_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AParser st SYMB_MAP_ITEMS -> PrefixMap -> AParser st SYMB_MAP_ITEMS
forall a b. a -> b -> a
const Maybe (AParser st SYMB_MAP_ITEMS)
forall st. Maybe (GenParser Char st SYMB_MAP_ITEMS)
parseSymbMapItems

-- | Instance of Logic for reduce logc
instance Logic CSL
    ()                        -- Sublogics
    BASIC_SPEC                -- basic_spec
    CMD                       -- sentences are CAS commands
    SYMB_ITEMS                -- symb_items
    SYMB_MAP_ITEMS            -- symb_map_items
    Sign                      -- sign
    Morphism                  -- morphism
    Symbol                    -- symbol
    Symbol                    -- raw_symbol
    [EXPRESSION]              -- proof_tree
    where
      stability :: CSL -> Stability
stability CSL = Stability
Experimental
      empty_proof_tree :: CSL -> [EXPRESSION]
empty_proof_tree CSL = []
      -- supplied provers
      provers :: CSL -> [Prover Sign CMD Morphism () [EXPRESSION]]
provers CSL = [Prover Sign CMD Morphism () [EXPRESSION]
reduceProver]

-- | Static Analysis for reduce logic
instance StaticAnalysis CSL
    BASIC_SPEC                -- basic_spec
    CMD                       -- sentence
    SYMB_ITEMS                -- symb_items
    SYMB_MAP_ITEMS            -- symb_map_items
    Sign                      -- sign
    Morphism                  -- morphism
    Symbol                    -- symbol
    Symbol                    -- raw_symbol
        where
          basic_analysis :: CSL
-> Maybe
     ((BASIC_SPEC, Sign, GlobalAnnos)
      -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD]))
basic_analysis CSL = ((BASIC_SPEC, Sign, GlobalAnnos)
 -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD]))
-> Maybe
     ((BASIC_SPEC, Sign, GlobalAnnos)
      -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD]))
forall a. a -> Maybe a
Just (BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])
forall a.
(BASIC_SPEC, Sign, a)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])
basicCSLAnalysis
          empty_signature :: CSL -> Sign
empty_signature CSL = Sign
emptySig
          is_subsig :: CSL -> Sign -> Sign -> Bool
is_subsig CSL = Sign -> Sign -> Bool
isSubSigOf
          subsig_inclusion :: CSL -> Sign -> Sign -> Result Morphism
subsig_inclusion CSL s :: Sign
s = Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism)
-> (Sign -> Morphism) -> Sign -> Result Morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Sign -> Morphism
inclusionMap Sign
s
          signature_union :: CSL -> Sign -> Sign -> Result Sign
signature_union CSL = Sign -> Sign -> Result Sign
sigUnion
          symbol_to_raw :: CSL -> Symbol -> Symbol
symbol_to_raw CSL = Symbol -> Symbol
symbolToRaw
          id_to_raw :: CSL -> Id -> Symbol
id_to_raw CSL = Id -> Symbol
idToRaw
{- matches       CSL            = Symbol.matches
stat_symb_items CSL          = mkStatSymbItems
stat_symb_map_items CSL      = mkStatSymbMapItem -}
          morphism_union :: CSL -> Morphism -> Morphism -> Result Morphism
morphism_union CSL = Morphism -> Morphism -> Result Morphism
morphismUnion
{- induced_from_morphism CSL    = inducedFromMorphism
induced_from_to_morphism CSL = inducedFromToMorphism -}