Logic_LF.hs revision b3bacd257ffcdd346b70ab690f03b28ad5f33fdc
8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
8a77240a809197c92c0736c431b4b88947a7bac1Christian MaederModule : $Header$
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian MaederDescription : Instances of classes defined in Logic.hs for the Edinburgh
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Logical Framework
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederCopyright : (c) Kristina Sojakova, DFKI Bremen 2009
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : k.sojakova@jacobs-university.de
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiStability : experimental
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiPortability : portable
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport qualified Data.Map as Map
1a38107941725211e7c3f051f7a8f5e12199f03acmaederdata LF = LF deriving Show
1a38107941725211e7c3f051f7a8f5e12199f03acmaederinstance Language LF where
d9a45a35cd696085be1a038b2cc67bee6819c574cmaeder description LF = "Edinburgh Logical Framework"
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance Category Sign Morphism where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder ide = idMorph
d9a45a35cd696085be1a038b2cc67bee6819c574cmaeder cod = target
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski composeMorphisms = compMorph
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski isInclusion = Map.null . symMap . canForm
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski legal_mor = const True
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance Syntax LF BASIC_SPEC SYMB_ITEMS SYMB_MAP_ITEMS where
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski parse_basic_spec LF = Just basicSpec
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder parse_symb_items LF = Just symbItems
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder parse_symb_map_items LF = Just symbMapItems
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Sentences LF
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder map_sen LF m = (Result []) . (translate m)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sym_of LF = singletonList . getSymbols
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiinstance Logic LF
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski SYMB_MAP_ITEMS
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance StaticAnalysis LF
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder basic_analysis LF = Just $ basicAnalysis
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder stat_symb_items LF = symbAnalysis
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder stat_symb_map_items LF = symbMapAnalysis
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder symbol_to_raw LF = symName
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski matches LF s1 s2 = symName s1 == s2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski empty_signature LF = emptySig
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder is_subsig LF = isSubsig
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder subsig_inclusion LF = inclusionMorph
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder signature_union LF = sigUnion
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski intersection LF = sigIntersection
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski generated_sign LF syms sig = do
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sig'<- genSig syms sig
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder inclusionMorph sig' sig
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski cogenerated_sign LF syms sig = do
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder sig'<- coGenSig syms sig
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder inclusionMorph sig' sig
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder induced_from_to_morphism LF m (ExtSign sig1 _) (ExtSign sig2 _) =
e7d2b3903c7b44db432538b0d720c21062c24823Christian Maeder inducedFromToMorphism (translMapAnalysis m sig1 sig2) sig1 sig2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiinstance LogicFram LF
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski SYMB_MAP_ITEMS
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski base_sig LF = baseSig
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski write_logic LF = writeLogic
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski write_syntax LF = writeSyntax