55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
b43458b4d81f7451112cecbd757f3a05216e7088Kristina SojakovaDescription : Instances of classes defined in Logic.hs for the Edinburgh
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova Logical Framework
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaCopyright : (c) Kristina Sojakova, DFKI Bremen 2009
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaMaintainer : k.sojakova@jacobs-university.de
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaStability : experimental
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaPortability : portable
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatovimport LF.MorphParser (readMorphism)
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport qualified Data.Map as Map
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovadata LF = LF deriving Show
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovainstance Language LF where
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova description LF = "Edinburgh Logical Framework"
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovainstance Category Sign Morphism where
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova composeMorphisms = compMorph
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova isInclusion = Map.null . symMap . canForm
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maederinstance Monoid BASIC_SPEC where
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder mempty = Basic_spec []
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder mappend (Basic_spec l1) (Basic_spec l2) = Basic_spec $ l1 ++ l2
a65c6747c9acbbebc93baba7bae94d2e3d8cdafbTill Mossakowskiinstance Syntax LF BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova parse_basic_spec LF = Just basicSpec
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova parse_symb_items LF = Just symbItems
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova parse_symb_map_items LF = Just symbMapItems
d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakovainstance Sentences LF
a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder map_sen LF m = Result [] . translate m
d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova sym_of LF = singletonList . getSymbols
8e4ceffda229add37bbcd2a8a3de776a3e57eae3mscodescu symKind LF _ = "const"
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance Logic LF
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova SYMB_MAP_ITEMS
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance StaticAnalysis LF
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova SYMB_MAP_ITEMS
a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder basic_analysis LF = Just basicAnalysis
80d2ec8f37d5ddec13c14b17b1bab01e9c94630aChristian Maeder stat_symb_items LF _ = symbAnalysis
a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder stat_symb_map_items LF _ _ = symbMapAnalysis
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova symbol_to_raw LF = symName
168d206b4e5fd436c98239a1b6629c651f54c8eeKristina Sojakova matches LF s1 s2 =
a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder not (isSym s2) || symName s1 == s2
a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder -- expressions are checked manually or symbols match by name
d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova empty_signature LF = emptySig
d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova is_subsig LF = isSubsig
d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova subsig_inclusion LF = inclusionMorph
abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova signature_union LF = sigUnion
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova intersection LF = sigIntersection
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova generated_sign LF syms sig = do
a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder sig' <- genSig syms sig
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova inclusionMorph sig' sig
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova cogenerated_sign LF syms sig = do
a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder sig' <- coGenSig syms sig
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova inclusionMorph sig' sig
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova induced_from_to_morphism LF m (ExtSign sig1 _) (ExtSign sig2 _) =
abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova inducedFromToMorphism (translMapAnalysis m sig1 sig2) sig1 sig2
168d206b4e5fd436c98239a1b6629c651f54c8eeKristina Sojakova induced_from_morphism LF m sig =
80d2ec8f37d5ddec13c14b17b1bab01e9c94630aChristian Maeder inducedFromMorphism (renamMapAnalysis m sig) sig
fe4a3f8471fb29021de18fbb50bb3f3a8bd9c693Mihai Codescuinstance LogicalFramework LF
e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova SYMB_MAP_ITEMS
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina Sojakova base_sig LF = baseSig
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina Sojakova write_logic LF = writeLogic
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina Sojakova write_syntax LF = writeSyntax
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov write_proof LF = writeProof
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov write_model LF = writeModel
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov write_comorphism LF = writeComorphism
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder read_morphism LF = readMorphism