{-# 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 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 Show
instance Language DFOL where
description DFOL = "First-Order Logic with Dependent Types\n" ++
"developed by F. Rabe"
-- instance of Category for DFOL
instance Category Sign Morphism where
ide = idMorph
dom = source
cod = target
isInclusion = Map.null . symMap . canForm
composeMorphisms = compMorph
legal_mor m = unless (isValidMorph m) $ fail "illegal DFOL morphism"
instance Monoid BASIC_SPEC where
mempty = Basic_spec []
mappend (Basic_spec l1) (Basic_spec l2) = Basic_spec $ l1 ++ l2
-- syntax for DFOL
instance Syntax DFOL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
parse_basic_spec DFOL = Just basicSpec
parse_symb_items DFOL = Just symbItems
parse_symb_map_items DFOL = Just symbMapItems
-- sentences for DFOL
instance Sentences DFOL FORMULA Sign Morphism Symbol where
map_sen DFOL m = wrapInResult . applyMorph m
sym_of DFOL = singletonList . Set.map Symbol . getSymbols
symmap_of DFOL = toSymMap . symMap
sym_name DFOL = toId
-- static analysis for DFOL
instance StaticAnalysis DFOL
BASIC_SPEC
FORMULA
SYMB_ITEMS
SYMB_MAP_ITEMS
Sign
Morphism
Symbol
Symbol
where
basic_analysis DFOL = Just basicAnalysis
stat_symb_map_items DFOL _ _ = symbMapAnalysis
stat_symb_items DFOL _ = symbAnalysis
symbol_to_raw DFOL = id
id_to_raw DFOL = fromId
matches DFOL s1 s2 = s1 == s2
empty_signature DFOL = emptySig
is_subsig DFOL sig1 sig2 = isValidMorph $ Morphism sig1 sig2 Map.empty
signature_union DFOL = sigUnion
intersection DFOL = sigIntersection
subsig_inclusion DFOL = inclusionMorph
morphism_union DFOL = morphUnion
induced_from_morphism DFOL = inducedFromMorphism
induced_from_to_morphism DFOL = inducedFromToMorphism
signature_colimit DFOL = sigColimit
generated_sign DFOL = coGenSig False
cogenerated_sign DFOL = coGenSig True
final_union DFOL = 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 x = Result [] $ Just x