{-# LANGUAGE MultiParamTypeClasses #-}
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
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 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 []
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
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
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
instance Logic DFOL
()
BASIC_SPEC
FORMULA
SYMB_ITEMS
SYMB_MAP_ITEMS
Sign
Morphism
Symbol
Symbol
()
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