{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Fpl/Logic_Fpl.hs
Description :  logic instance for FPL
Copyright   :  (c) Christian Maeder, DFKI GmbH 2011
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable

Instance of class Logic for FPL.
-}

module Fpl.Logic_Fpl where

import Logic.Logic

import Fpl.As
import Fpl.Sign
import Fpl.StatAna
import Fpl.Morphism
import Fpl.ATC_Fpl ()

import CASL.Sign
import CASL.Morphism
import CASL.SymbolMapAnalysis
import CASL.AS_Basic_CASL
import CASL.Parse_AS_Basic
import CASL.SimplifySen
import CASL.SymbolParser
import CASL.Taxonomy
import CASL.Logic_CASL ()

import Common.DocUtils

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

instance Language Fpl where
  description :: Fpl -> String
description _ = [String] -> String
unlines
    [ "logic of functional programs (FPL) as CASL extension" ]

instance SignExtension SignExt where
  isSubSignExtension :: SignExt -> SignExt -> Bool
isSubSignExtension = SignExt -> SignExt -> Bool
isSubFplSign

instance Syntax Fpl FplBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
    parse_basic_spec :: Fpl -> Maybe (PrefixMap -> AParser st FplBasicSpec)
parse_basic_spec Fpl = (PrefixMap -> AParser st FplBasicSpec)
-> Maybe (PrefixMap -> AParser st FplBasicSpec)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st FplBasicSpec)
 -> Maybe (PrefixMap -> AParser st FplBasicSpec))
-> (PrefixMap -> AParser st FplBasicSpec)
-> Maybe (PrefixMap -> AParser st FplBasicSpec)
forall a b. (a -> b) -> a -> b
$ [String] -> PrefixMap -> AParser st FplBasicSpec
forall f s b st.
(TermParser f, AParsable s, AParsable b) =>
[String] -> PrefixMap -> AParser st (BASIC_SPEC b s f)
basicSpec [String]
fplReservedWords
    parse_symb_items :: Fpl -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items Fpl = (PrefixMap -> AParser st SYMB_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> (AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS)
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st SYMB_ITEMS
forall st. [String] -> AParser st SYMB_ITEMS
symbItems [String]
fplReservedWords
    parse_symb_map_items :: Fpl -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items Fpl = (PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_MAP_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> (AParser st SYMB_MAP_ITEMS
    -> PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_MAP_ITEMS -> PrefixMap -> AParser st SYMB_MAP_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_MAP_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st SYMB_MAP_ITEMS
forall st. [String] -> AParser st SYMB_MAP_ITEMS
symbMapItems [String]
fplReservedWords

instance Sentences Fpl FplForm FplSign FplMor Symbol where
      map_sen :: Fpl -> FplMor -> FplForm -> Result FplForm
map_sen Fpl m :: FplMor
m = FplForm -> Result FplForm
forall (m :: * -> *) a. Monad m => a -> m a
return (FplForm -> Result FplForm)
-> (FplForm -> FplForm) -> FplForm -> Result FplForm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FplMor -> FplForm -> FplForm
mapFplSen FplMor
m
      sym_of :: Fpl -> FplSign -> [Set Symbol]
sym_of Fpl = FplSign -> [Set Symbol]
forall f e. Sign f e -> [Set Symbol]
symOf
      symKind :: Fpl -> Symbol -> String
symKind Fpl = 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
. SYMB_KIND -> Doc
forall a. Pretty a => a -> Doc
pretty (SYMB_KIND -> Doc) -> (Symbol -> SYMB_KIND) -> Symbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbType -> SYMB_KIND
symbolKind (SymbType -> SYMB_KIND)
-> (Symbol -> SymbType) -> Symbol -> SYMB_KIND
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> SymbType
symbType
      symmap_of :: Fpl -> FplMor -> EndoMap Symbol
symmap_of Fpl = FplMor -> EndoMap Symbol
forall f e m. Morphism f e m -> EndoMap Symbol
morphismToSymbMap
      sym_name :: Fpl -> Symbol -> Id
sym_name Fpl = Symbol -> Id
symName
      simplify_sen :: Fpl -> FplSign -> FplForm -> FplForm
simplify_sen Fpl = Min TermExt SignExt
-> (FplSign -> TermExt -> TermExt) -> FplSign -> FplForm -> FplForm
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min TermExt SignExt
minFplTerm FplSign -> TermExt -> TermExt
simplifyTermExt (FplSign -> FplForm -> FplForm)
-> (FplSign -> FplSign) -> FplSign -> FplForm -> FplForm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FplSign -> FplSign
addBuiltins

instance StaticAnalysis Fpl FplBasicSpec FplForm
               SYMB_ITEMS SYMB_MAP_ITEMS
               FplSign
               FplMor
               Symbol RawSymbol where
         basic_analysis :: Fpl
-> Maybe
     ((FplBasicSpec, FplSign, GlobalAnnos)
      -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm]))
basic_analysis Fpl = ((FplBasicSpec, FplSign, GlobalAnnos)
 -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm]))
-> Maybe
     ((FplBasicSpec, FplSign, GlobalAnnos)
      -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm]))
forall a. a -> Maybe a
Just (FplBasicSpec, FplSign, GlobalAnnos)
-> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])
basicFplAnalysis
         stat_symb_map_items :: Fpl
-> FplSign
-> Maybe FplSign
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
stat_symb_map_items Fpl = FplSign
-> Maybe FplSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol)
forall f e.
Sign f e
-> Maybe (Sign f e)
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
statSymbMapItems
         stat_symb_items :: Fpl -> FplSign -> [SYMB_ITEMS] -> Result [RawSymbol]
stat_symb_items Fpl = FplSign -> [SYMB_ITEMS] -> Result [RawSymbol]
forall f e. Sign f e -> [SYMB_ITEMS] -> Result [RawSymbol]
statSymbItems

         symbol_to_raw :: Fpl -> Symbol -> RawSymbol
symbol_to_raw Fpl = Symbol -> RawSymbol
symbolToRaw
         id_to_raw :: Fpl -> Id -> RawSymbol
id_to_raw Fpl = Id -> RawSymbol
idToRaw
         matches :: Fpl -> Symbol -> RawSymbol -> Bool
matches Fpl = Symbol -> RawSymbol -> Bool
CASL.Morphism.matches

         empty_signature :: Fpl -> FplSign
empty_signature Fpl = SignExt -> FplSign
forall e f. e -> Sign f e
emptySign SignExt
emptyFplSign
         signature_union :: Fpl -> FplSign -> FplSign -> Result FplSign
signature_union Fpl s :: FplSign
s = FplSign -> Result FplSign
forall (m :: * -> *) a. Monad m => a -> m a
return (FplSign -> Result FplSign)
-> (FplSign -> FplSign) -> FplSign -> Result FplSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SignExt -> SignExt -> SignExt) -> FplSign -> FplSign -> FplSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig SignExt -> SignExt -> SignExt
addFplSign FplSign
s
         signatureDiff :: Fpl -> FplSign -> FplSign -> Result FplSign
signatureDiff Fpl s :: FplSign
s = FplSign -> Result FplSign
forall (m :: * -> *) a. Monad m => a -> m a
return (FplSign -> Result FplSign)
-> (FplSign -> FplSign) -> FplSign -> Result FplSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SignExt -> SignExt -> SignExt) -> FplSign -> FplSign -> FplSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
diffSig SignExt -> SignExt -> SignExt
diffFplSign FplSign
s
         intersection :: Fpl -> FplSign -> FplSign -> Result FplSign
intersection Fpl s :: FplSign
s = FplSign -> Result FplSign
forall (m :: * -> *) a. Monad m => a -> m a
return (FplSign -> Result FplSign)
-> (FplSign -> FplSign) -> FplSign -> Result FplSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SignExt -> SignExt -> SignExt) -> FplSign -> FplSign -> FplSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
interSig SignExt -> SignExt -> SignExt
interFplSign FplSign
s
         morphism_union :: Fpl -> FplMor -> FplMor -> Result FplMor
morphism_union Fpl = (SignExt -> SignExt -> SignExt)
-> FplMor -> FplMor -> Result FplMor
forall e f m.
(e -> e -> e)
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
plainMorphismUnion SignExt -> SignExt -> SignExt
addFplSign
         final_union :: Fpl -> FplSign -> FplSign -> Result FplSign
final_union Fpl = (SignExt -> SignExt -> SignExt)
-> FplSign -> FplSign -> Result FplSign
forall e f.
(e -> e -> e) -> Sign f e -> Sign f e -> Result (Sign f e)
finalUnion SignExt -> SignExt -> SignExt
addFplSign
         is_subsig :: Fpl -> FplSign -> FplSign -> Bool
is_subsig Fpl = (SignExt -> SignExt -> Bool) -> FplSign -> FplSign -> Bool
forall e f. (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
isSubSig SignExt -> SignExt -> Bool
isSubFplSign
         subsig_inclusion :: Fpl -> FplSign -> FplSign -> Result FplMor
subsig_inclusion Fpl = DefMorExt SignExt -> FplSign -> FplSign -> Result FplMor
forall m f e. m -> Sign f e -> Sign f e -> Result (Morphism f e m)
sigInclusion DefMorExt SignExt
forall e. DefMorExt e
emptyMorExt
         cogenerated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor
cogenerated_sign Fpl = DefMorExt SignExt -> Set Symbol -> FplSign -> Result FplMor
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
cogeneratedSign DefMorExt SignExt
forall e. DefMorExt e
emptyMorExt
         generated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor
generated_sign Fpl = DefMorExt SignExt -> Set Symbol -> FplSign -> Result FplMor
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
generatedSign DefMorExt SignExt
forall e. DefMorExt e
emptyMorExt
         induced_from_morphism :: Fpl -> EndoMap RawSymbol -> FplSign -> Result FplMor
induced_from_morphism Fpl = DefMorExt SignExt -> EndoMap RawSymbol -> FplSign -> Result FplMor
forall e f m.
(Pretty e, Show f) =>
m -> EndoMap RawSymbol -> Sign f e -> Result (Morphism f e m)
inducedFromMorphism DefMorExt SignExt
forall e. DefMorExt e
emptyMorExt
         induced_from_to_morphism :: Fpl
-> EndoMap RawSymbol
-> ExtSign FplSign Symbol
-> ExtSign FplSign Symbol
-> Result FplMor
induced_from_to_morphism Fpl =
             DefMorExt SignExt
-> (SignExt -> SignExt -> Bool)
-> (SignExt -> SignExt -> SignExt)
-> EndoMap RawSymbol
-> ExtSign FplSign Symbol
-> ExtSign FplSign Symbol
-> Result FplMor
forall e f m.
(Eq e, Show f, Pretty e, Pretty m) =>
m
-> (e -> e -> Bool)
-> (e -> e -> e)
-> EndoMap RawSymbol
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol
-> Result (Morphism f e m)
inducedFromToMorphism DefMorExt SignExt
forall e. DefMorExt e
emptyMorExt SignExt -> SignExt -> Bool
isSubFplSign SignExt -> SignExt -> SignExt
diffFplSign
         theory_to_taxonomy :: Fpl
-> TaxoGraphKind
-> MMiSSOntology
-> FplSign
-> [Named FplForm]
-> Result MMiSSOntology
theory_to_taxonomy Fpl = TaxoGraphKind
-> MMiSSOntology
-> FplSign
-> [Named FplForm]
-> Result MMiSSOntology
forall f e.
TaxoGraphKind
-> MMiSSOntology
-> Sign f e
-> [Named (FORMULA f)]
-> Result MMiSSOntology
convTaxo

instance Logic Fpl ()
               FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS
               FplSign
               FplMor
               Symbol RawSymbol () where
         stability :: Fpl -> Stability
stability _ = Stability
Experimental
         empty_proof_tree :: Fpl -> ()
empty_proof_tree _ = ()