{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./LF/Logic_LF.hs
Description :  Instances of classes defined in Logic.hs for the Edinburgh
               Logical Framework
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

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

module LF.Logic_LF where

import LF.AS
import LF.Parse
import LF.MorphParser (readMorphism)
import LF.Sign
import LF.Morphism
import LF.ATC_LF ()
import LF.Analysis
import LF.Framework
import LF.ComorphFram ()

import Logic.Logic

import Common.Result
import Common.ExtSign

import qualified Data.Map as Map
import Data.Monoid ()

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

instance Language LF where
   description :: LF -> String
description LF = "Edinburgh Logical Framework"

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
   composeMorphisms :: Morphism -> Morphism -> Result Morphism
composeMorphisms = Morphism -> Morphism -> Result Morphism
compMorph
   isInclusion :: Morphism -> Bool
isInclusion = Map Symbol EXP -> Bool
forall k a. Map k a -> Bool
Map.null (Map Symbol EXP -> Bool)
-> (Morphism -> Map Symbol EXP) -> Morphism -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Map Symbol EXP
symMap (Morphism -> Map Symbol EXP)
-> (Morphism -> Morphism) -> Morphism -> Map Symbol EXP
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Morphism
canForm

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 LF BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
   parse_basic_spec :: LF -> Maybe (PrefixMap -> AParser st BASIC_SPEC)
parse_basic_spec LF = (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 :: LF -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items LF = (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 :: LF -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items LF = (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 LF
   Sentence
   Sign
   Morphism
   Symbol
   where
   map_sen :: LF -> Morphism -> EXP -> Result EXP
map_sen LF m :: Morphism
m = [Diagnosis] -> Maybe EXP -> Result EXP
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] (Maybe EXP -> Result EXP)
-> (EXP -> Maybe EXP) -> EXP -> Result EXP
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> EXP -> Maybe EXP
translate Morphism
m
   sym_of :: LF -> Sign -> [Set Symbol]
sym_of LF = 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
. Sign -> Set Symbol
getSymbols
   symKind :: LF -> Symbol -> String
symKind LF _ = "const"

instance Logic LF
   ()
   BASIC_SPEC
   Sentence
   SYMB_ITEMS
   SYMB_MAP_ITEMS
   Sign
   Morphism
   Symbol
   RAW_SYM
   ()

instance StaticAnalysis LF
   BASIC_SPEC
   Sentence
   SYMB_ITEMS
   SYMB_MAP_ITEMS
   Sign
   Morphism
   Symbol
   RAW_SYM
   where
   basic_analysis :: LF
-> Maybe
     ((BASIC_SPEC, Sign, GlobalAnnos)
      -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named EXP]))
basic_analysis LF = ((BASIC_SPEC, Sign, GlobalAnnos)
 -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named EXP]))
-> Maybe
     ((BASIC_SPEC, Sign, GlobalAnnos)
      -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named EXP]))
forall a. a -> Maybe a
Just (BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named EXP])
basicAnalysis
   stat_symb_items :: LF -> Sign -> [SYMB_ITEMS] -> Result [String]
stat_symb_items LF _ = [SYMB_ITEMS] -> Result [String]
symbAnalysis
   stat_symb_map_items :: LF
-> Sign
-> Maybe Sign
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap String)
stat_symb_map_items LF _ _ = [SYMB_MAP_ITEMS] -> Result (EndoMap String)
symbMapAnalysis
   symbol_to_raw :: LF -> Symbol -> String
symbol_to_raw LF = Symbol -> String
symName
   matches :: LF -> Symbol -> String -> Bool
matches LF s1 :: Symbol
s1 s2 :: String
s2 =
     Bool -> Bool
not (String -> Bool
isSym String
s2) Bool -> Bool -> Bool
|| Symbol -> String
symName Symbol
s1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
s2
     -- expressions are checked manually or symbols match by name
   empty_signature :: LF -> Sign
empty_signature LF = Sign
emptySig
   is_subsig :: LF -> Sign -> Sign -> Bool
is_subsig LF = Sign -> Sign -> Bool
isSubsig
   subsig_inclusion :: LF -> Sign -> Sign -> Result Morphism
subsig_inclusion LF = Sign -> Sign -> Result Morphism
inclusionMorph
   signature_union :: LF -> Sign -> Sign -> Result Sign
signature_union LF = Sign -> Sign -> Result Sign
sigUnion
   intersection :: LF -> Sign -> Sign -> Result Sign
intersection LF = Sign -> Sign -> Result Sign
sigIntersection
   generated_sign :: LF -> Set Symbol -> Sign -> Result Morphism
generated_sign LF syms :: Set Symbol
syms sig :: Sign
sig = do
     Sign
sig' <- Set Symbol -> Sign -> Result Sign
genSig Set Symbol
syms Sign
sig
     Sign -> Sign -> Result Morphism
inclusionMorph Sign
sig' Sign
sig
   cogenerated_sign :: LF -> Set Symbol -> Sign -> Result Morphism
cogenerated_sign LF syms :: Set Symbol
syms sig :: Sign
sig = do
     Sign
sig' <- Set Symbol -> Sign -> Result Sign
coGenSig Set Symbol
syms Sign
sig
     Sign -> Sign -> Result Morphism
inclusionMorph Sign
sig' Sign
sig
   induced_from_to_morphism :: LF
-> EndoMap String
-> ExtSign Sign Symbol
-> ExtSign Sign Symbol
-> Result Morphism
induced_from_to_morphism LF m :: EndoMap String
m (ExtSign sig1 :: Sign
sig1 _) (ExtSign sig2 :: Sign
sig2 _) =
     Map Symbol (EXP, EXP) -> Sign -> Sign -> Result Morphism
inducedFromToMorphism (EndoMap String -> Sign -> Sign -> Map Symbol (EXP, EXP)
translMapAnalysis EndoMap String
m Sign
sig1 Sign
sig2) Sign
sig1 Sign
sig2
   induced_from_morphism :: LF -> EndoMap String -> Sign -> Result Morphism
induced_from_morphism LF m :: EndoMap String
m sig :: Sign
sig =
     EndoMap Symbol -> Sign -> Result Morphism
inducedFromMorphism (EndoMap String -> Sign -> EndoMap Symbol
renamMapAnalysis EndoMap String
m Sign
sig) Sign
sig

instance LogicalFramework LF
   ()
   BASIC_SPEC
   Sentence
   SYMB_ITEMS
   SYMB_MAP_ITEMS
   Sign
   Morphism
   Symbol
   RAW_SYM
   ()
   where
   base_sig :: LF -> Sign
base_sig LF = Sign
baseSig
   write_logic :: LF -> ShowS
write_logic LF = ShowS
writeLogic
   write_syntax :: LF -> String -> Morphism -> String
write_syntax LF = String -> Morphism -> String
writeSyntax
   write_proof :: LF -> String -> Morphism -> String
write_proof LF = String -> Morphism -> String
writeProof
   write_model :: LF -> String -> Morphism -> String
write_model LF = String -> Morphism -> String
writeModel
   write_comorphism :: LF
-> String
-> String
-> String
-> Morphism
-> Morphism
-> Morphism
-> String
write_comorphism LF = String
-> String -> String -> Morphism -> Morphism -> Morphism -> String
writeComorphism
   read_morphism :: LF -> String -> Morphism
read_morphism LF = String -> Morphism
readMorphism