{-# 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
