{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Adl/Logic_Adl.hs
Description :  the Logic instance for ADL
Copyright   :  (c) Stef Joosten, Christian Maeder DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (import Logic.Logic)

see
Stef Joosten:
Deriving Functional Specifications from Business Requirements with Ampersand

and
https://lab.cs.ru.nl/BusinessRules/Requirements_engineering
-}

module Adl.Logic_Adl where

import Adl.As
import Adl.Parse
import Adl.Print ()
import Adl.Sign
import Adl.StatAna
import Adl.ATC_Adl ()

import ATC.ProofTree ()

import Common.DefaultMorphism
import Common.ProofTree
import Common.DocUtils

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

import Logic.Logic

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

instance Language Adl where
    description :: Adl -> String
description _ = "A description language for business rules"

type Morphism = DefaultMorphism Sign

instance Sentences Adl
    Sen
    Sign
    Morphism
    Symbol
    where
      sym_of :: Adl -> Sign -> [Set Symbol]
sym_of Adl = 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
      symmap_of :: Adl -> Morphism -> EndoMap Symbol
symmap_of Adl _ = EndoMap Symbol
forall k a. Map k a
Map.empty
      sym_name :: Adl -> Symbol -> Id
sym_name Adl = Symbol -> Id
symName
      map_sen :: Adl -> Morphism -> Sen -> Result Sen
map_sen Adl _ = Sen -> Result Sen
forall (m :: * -> *) a. Monad m => a -> m a
return (Sen -> Result Sen) -> (Sen -> Sen) -> Sen -> Result Sen
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sen -> Sen
forall a. a -> a
id
      print_named :: Adl -> Named Sen -> Doc
print_named Adl = Named Sen -> Doc
printNSen
      symKind :: Adl -> Symbol -> String
symKind Adl = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Symbol -> Doc) -> Symbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolKind -> Doc
forall a. Pretty a => a -> Doc
pretty (SymbolKind -> Doc) -> (Symbol -> SymbolKind) -> Symbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> SymbolKind
sym_kind

instance Semigroup Context where
    (Context m1 :: Maybe Token
m1 l1 :: [PatElem]
l1) <> :: Context -> Context -> Context
<> (Context m2 :: Maybe Token
m2 l2 :: [PatElem]
l2) = Maybe Token -> [PatElem] -> Context
Context (Maybe Token -> Maybe Token -> Maybe Token
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus Maybe Token
m1 Maybe Token
m2) ([PatElem] -> Context) -> [PatElem] -> Context
forall a b. (a -> b) -> a -> b
$ [PatElem]
l1 [PatElem] -> [PatElem] -> [PatElem]
forall a. [a] -> [a] -> [a]
++ [PatElem]
l2
instance Monoid Context where
    mempty :: Context
mempty = Maybe Token -> [PatElem] -> Context
Context Maybe Token
forall a. Maybe a
Nothing []

instance Syntax Adl
    Context
    Symbol
    ()
    ()
    where
      parse_basic_spec :: Adl -> Maybe (PrefixMap -> AParser st Context)
parse_basic_spec Adl = (PrefixMap -> AParser st Context)
-> Maybe (PrefixMap -> AParser st Context)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st Context)
 -> Maybe (PrefixMap -> AParser st Context))
-> (PrefixMap -> AParser st Context)
-> Maybe (PrefixMap -> AParser st Context)
forall a b. (a -> b) -> a -> b
$ AParser st Context -> PrefixMap -> AParser st Context
forall a b. a -> b -> a
const AParser st Context
forall st. CharParser st Context
pArchitecture
      parse_symb_items :: Adl -> Maybe (PrefixMap -> AParser st ())
parse_symb_items Adl = Maybe (PrefixMap -> AParser st ())
forall a. Maybe a
Nothing
      parse_symb_map_items :: Adl -> Maybe (PrefixMap -> AParser st ())
parse_symb_map_items Adl = Maybe (PrefixMap -> AParser st ())
forall a. Maybe a
Nothing

instance Logic Adl
    ()                -- Sublogics
    Context           -- basic_spec
    Sen               -- sentence
    ()                -- symb_items
    ()                -- symb_map_items
    Sign              -- sign
    Morphism          -- morphism
    Symbol            -- symbol
    RawSymbol         -- raw_symbol
    ProofTree         -- proof_tree
    where
       empty_proof_tree :: Adl -> ProofTree
empty_proof_tree Adl = ProofTree
emptyProofTree
       provers :: Adl -> [Prover Sign Sen Morphism () ProofTree]
provers Adl = []
       stability :: Adl -> Stability
stability Adl = Stability
Testing

instance StaticAnalysis Adl
    Context
    Sen
    ()
    ()
    Sign
    Morphism
    Symbol
    RawSymbol
    where
      basic_analysis :: Adl
-> Maybe
     ((Context, Sign, GlobalAnnos)
      -> Result (Context, ExtSign Sign Symbol, [Named Sen]))
basic_analysis Adl = ((Context, Sign, GlobalAnnos)
 -> Result (Context, ExtSign Sign Symbol, [Named Sen]))
-> Maybe
     ((Context, Sign, GlobalAnnos)
      -> Result (Context, ExtSign Sign Symbol, [Named Sen]))
forall a. a -> Maybe a
Just (Context, Sign, GlobalAnnos)
-> Result (Context, ExtSign Sign Symbol, [Named Sen])
basicAna
      empty_signature :: Adl -> Sign
empty_signature Adl = Sign
emptySign
      is_subsig :: Adl -> Sign -> Sign -> Bool
is_subsig Adl = Sign -> Sign -> Bool
isSubSignOf
      signature_union :: Adl -> Sign -> Sign -> Result Sign
signature_union Adl = Sign -> Sign -> Result Sign
signUnion
      symbol_to_raw :: Adl -> Symbol -> RawSymbol
symbol_to_raw Adl = Symbol -> RawSymbol
Symbol
      matches :: Adl -> Symbol -> RawSymbol -> Bool
matches Adl = Symbol -> RawSymbol -> Bool
symMatch