{-# LANGUAGE MultiParamTypeClasses #-}
{- |
Module      :  ./DFOL/Logic_DFOL.hs
Description :  Instances of classes defined in Logic.hs for first-order logic
               with dependent types (DFOL)
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  k.sojakova@jacobs-university.de
Stability   :  experimental
Portability :  portable

Ref: Florian Rabe: First-Order Logic with Dependent Types.
     IJCAR 2006, pages 377-391.
-}

module DFOL.Logic_DFOL where

import Common.Result

import Data.Monoid ()
import qualified Data.Map as Map
import qualified Data.Set as Set
import Control.Monad (unless)
import qualified Control.Monad.Fail as Fail

import DFOL.AS_DFOL
import DFOL.Sign
import DFOL.Morphism
import DFOL.Parse_AS_DFOL
import DFOL.ATC_DFOL ()
import DFOL.Analysis_DFOL
import DFOL.Symbol
import DFOL.Colimit

import Logic.Logic

-- lid for first-order logic with dependent types
data DFOL = DFOL deriving Int -> DFOL -> ShowS
[DFOL] -> ShowS
DFOL -> String
(Int -> DFOL -> ShowS)
-> (DFOL -> String) -> ([DFOL] -> ShowS) -> Show DFOL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DFOL] -> ShowS
$cshowList :: [DFOL] -> ShowS
show :: DFOL -> String
$cshow :: DFOL -> String
showsPrec :: Int -> DFOL -> ShowS
$cshowsPrec :: Int -> DFOL -> ShowS
Show

instance Language DFOL where
   description :: DFOL -> String
description DFOL = "First-Order Logic with Dependent Types\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                      "developed by F. Rabe"

-- instance of Category for DFOL
instance Category Sign Morphism where
   ide :: Sign -> Morphism
ide = Sign -> Morphism
idMorph
   dom :: Morphism -> Sign
dom = Morphism -> Sign
source
   cod :: Morphism -> Sign
cod = Morphism -> Sign
target
   isInclusion :: Morphism -> Bool
isInclusion = Map NAME NAME -> Bool
forall k a. Map k a -> Bool
Map.null (Map NAME NAME -> Bool)
-> (Morphism -> Map NAME NAME) -> Morphism -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Map NAME NAME
symMap (Morphism -> Map NAME NAME)
-> (Morphism -> Morphism) -> Morphism -> Map NAME NAME
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Morphism
canForm
   composeMorphisms :: Morphism -> Morphism -> Result Morphism
composeMorphisms = Morphism -> Morphism -> Result Morphism
compMorph
   legal_mor :: Morphism -> Result ()
legal_mor m :: Morphism
m = Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Morphism -> Bool
isValidMorph Morphism
m) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "illegal DFOL morphism"

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 for DFOL
instance Syntax DFOL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
   parse_basic_spec :: DFOL -> Maybe (PrefixMap -> AParser st BASIC_SPEC)
parse_basic_spec DFOL = (PrefixMap -> AParser st BASIC_SPEC)
-> Maybe (PrefixMap -> AParser st BASIC_SPEC)
forall a. a -> Maybe a
Just PrefixMap -> AParser st BASIC_SPEC
forall st. PrefixMap -> AParser st BASIC_SPEC
basicSpec
   parse_symb_items :: DFOL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items DFOL = (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
$ AParser st SYMB_ITEMS
forall st. AParser st SYMB_ITEMS
symbItems
   parse_symb_map_items :: DFOL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items DFOL = (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
$ AParser st SYMB_MAP_ITEMS
forall st. AParser st SYMB_MAP_ITEMS
symbMapItems

-- sentences for DFOL
instance Sentences DFOL FORMULA Sign Morphism Symbol where
   map_sen :: DFOL -> Morphism -> FORMULA -> Result FORMULA
map_sen DFOL m :: Morphism
m = FORMULA -> Result FORMULA
forall a. a -> Result a
wrapInResult (FORMULA -> Result FORMULA)
-> (FORMULA -> FORMULA) -> FORMULA -> Result FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> FORMULA -> FORMULA
forall a. Translatable a => Morphism -> a -> a
applyMorph Morphism
m
   sym_of :: DFOL -> Sign -> [Set Symbol]
sym_of DFOL = 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
. (NAME -> Symbol) -> Set NAME -> Set Symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map NAME -> Symbol
Symbol (Set NAME -> Set Symbol)
-> (Sign -> Set NAME) -> Sign -> Set Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Set NAME
getSymbols
   symmap_of :: DFOL -> Morphism -> EndoMap Symbol
symmap_of DFOL = Map NAME NAME -> EndoMap Symbol
toSymMap (Map NAME NAME -> EndoMap Symbol)
-> (Morphism -> Map NAME NAME) -> Morphism -> EndoMap Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Map NAME NAME
symMap
   sym_name :: DFOL -> Symbol -> Id
sym_name DFOL = Symbol -> Id
toId

-- static analysis for DFOL
instance StaticAnalysis DFOL
   BASIC_SPEC
   FORMULA
   SYMB_ITEMS
   SYMB_MAP_ITEMS
   Sign
   Morphism
   Symbol
   Symbol
   where
   basic_analysis :: DFOL
-> Maybe
     ((BASIC_SPEC, Sign, GlobalAnnos)
      -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA]))
basic_analysis DFOL = ((BASIC_SPEC, Sign, GlobalAnnos)
 -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA]))
-> Maybe
     ((BASIC_SPEC, Sign, GlobalAnnos)
      -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA]))
forall a. a -> Maybe a
Just (BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
basicAnalysis
   stat_symb_map_items :: DFOL
-> Sign
-> Maybe Sign
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap Symbol)
stat_symb_map_items DFOL _ _ = [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol)
symbMapAnalysis
   stat_symb_items :: DFOL -> Sign -> [SYMB_ITEMS] -> Result [Symbol]
stat_symb_items DFOL _ = [SYMB_ITEMS] -> Result [Symbol]
symbAnalysis
   symbol_to_raw :: DFOL -> Symbol -> Symbol
symbol_to_raw DFOL = Symbol -> Symbol
forall a. a -> a
id
   id_to_raw :: DFOL -> Id -> Symbol
id_to_raw DFOL = Id -> Symbol
fromId
   matches :: DFOL -> Symbol -> Symbol -> Bool
matches DFOL s1 :: Symbol
s1 s2 :: Symbol
s2 = Symbol
s1 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
s2
   empty_signature :: DFOL -> Sign
empty_signature DFOL = Sign
emptySig
   is_subsig :: DFOL -> Sign -> Sign -> Bool
is_subsig DFOL sig1 :: Sign
sig1 sig2 :: Sign
sig2 = Morphism -> Bool
isValidMorph (Morphism -> Bool) -> Morphism -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Sign -> Map NAME NAME -> Morphism
Morphism Sign
sig1 Sign
sig2 Map NAME NAME
forall k a. Map k a
Map.empty
   signature_union :: DFOL -> Sign -> Sign -> Result Sign
signature_union DFOL = Sign -> Sign -> Result Sign
sigUnion
   intersection :: DFOL -> Sign -> Sign -> Result Sign
intersection DFOL = Sign -> Sign -> Result Sign
sigIntersection
   subsig_inclusion :: DFOL -> Sign -> Sign -> Result Morphism
subsig_inclusion DFOL = Sign -> Sign -> Result Morphism
inclusionMorph
   morphism_union :: DFOL -> Morphism -> Morphism -> Result Morphism
morphism_union DFOL = Morphism -> Morphism -> Result Morphism
morphUnion
   induced_from_morphism :: DFOL -> EndoMap Symbol -> Sign -> Result Morphism
induced_from_morphism DFOL = EndoMap Symbol -> Sign -> Result Morphism
inducedFromMorphism
   induced_from_to_morphism :: DFOL
-> EndoMap Symbol
-> ExtSign Sign Symbol
-> ExtSign Sign Symbol
-> Result Morphism
induced_from_to_morphism DFOL = EndoMap Symbol
-> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism
inducedFromToMorphism
   signature_colimit :: DFOL -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism)
signature_colimit DFOL = Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism)
sigColimit
   generated_sign :: DFOL -> Set Symbol -> Sign -> Result Morphism
generated_sign DFOL = Bool -> Set Symbol -> Sign -> Result Morphism
coGenSig Bool
False
   cogenerated_sign :: DFOL -> Set Symbol -> Sign -> Result Morphism
cogenerated_sign DFOL = Bool -> Set Symbol -> Sign -> Result Morphism
coGenSig Bool
True
   final_union :: DFOL -> Sign -> Sign -> Result Sign
final_union DFOL = Sign -> Sign -> Result Sign
sigUnion        -- in DFOL every signature union is final

-- instance of logic for DFOL
instance Logic DFOL
   ()
   BASIC_SPEC
   FORMULA
   SYMB_ITEMS
   SYMB_MAP_ITEMS
   Sign
   Morphism
   Symbol
   Symbol
   ()

-- creates a Result
wrapInResult :: a -> Result a
wrapInResult :: a -> Result a
wrapInResult x :: a
x = [Diagnosis] -> Maybe a -> Result a
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] (Maybe a -> Result a) -> Maybe a -> Result a
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
x