842ae4bd224140319ae7feec1872b93dfd491143fielding{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

842ae4bd224140319ae7feec1872b93dfd491143fielding{- |

842ae4bd224140319ae7feec1872b93dfd491143fieldingModule : $Header$

842ae4bd224140319ae7feec1872b93dfd491143fieldingDescription : Instances of classes defined in Logic.hs for the Edinburgh

842ae4bd224140319ae7feec1872b93dfd491143fielding Logical Framework

842ae4bd224140319ae7feec1872b93dfd491143fieldingCopyright : (c) Kristina Sojakova, DFKI Bremen 2009

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrseLicense : GPLv2 or higher, see LICENSE.txt

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrseMaintainer : k.sojakova@jacobs-university.de

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndStability : experimental

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndPortability : portable

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd-}

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndmodule LF.Logic_LF where

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndimport LF.AS

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndimport LF.Parse

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndimport LF.MorphParser (readMorphism)

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndimport LF.Sign

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndimport LF.Morphism

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndimport LF.ATC_LF ()

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndimport LF.Analysis

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndimport LF.Framework

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndimport LF.ComorphFram ()

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrseimport Logic.Logic

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrseimport Common.Result

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrseimport Common.ExtSign

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse

e18e68b42830409bf48de0df9eed3fe363664aa7aaronimport qualified Data.Map as Map

70535d6421eb979ac79d8f49d31cd94d75dd8b2fjorton

8464a9c46b967001e38fe3c8afff51a649e9de51dougmdata LF = LF deriving Show

579fd9e90990eee18b5e504eb4c0d2ce18f76208aaron

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrseinstance Language LF where

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse description LF = "Edinburgh Logical Framework"

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrseinstance Category Sign Morphism where

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse ide = idMorph

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse dom = source

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse cod = target

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse composeMorphisms = compMorph

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse isInclusion = Map.null . symMap . canForm

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrseinstance Syntax LF BASIC_SPEC SYMB_ITEMS SYMB_MAP_ITEMS where

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse parse_basic_spec LF = Just basicSpec

05413593151a238718198cc04ca849b2426be106rse parse_symb_items LF = Just symbItems

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse parse_symb_map_items LF = Just symbMapItems

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrseinstance Sentences LF

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse Sentence

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse Sign

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse Morphism

434ad3e8e769a6a7a78c15f3ae2f7ae3adbfbb49wrowe Symbol

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse where

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse map_sen LF m = Result [] . translate m

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse sym_of LF = singletonList . getSymbols

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse

05413593151a238718198cc04ca849b2426be106rseinstance Logic LF

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse ()

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse BASIC_SPEC

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse Sentence

87a1c79b7b37702a254920ca5214fb282a4fb085dougm SYMB_ITEMS

87a1c79b7b37702a254920ca5214fb282a4fb085dougm SYMB_MAP_ITEMS

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse Sign

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse Morphism

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse Symbol

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse RAW_SYM

e8f95a682820a599fe41b22977010636be5c2717jim ()

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse

e8f95a682820a599fe41b22977010636be5c2717jiminstance StaticAnalysis LF

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse BASIC_SPEC

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse Sentence

e8f95a682820a599fe41b22977010636be5c2717jim SYMB_ITEMS

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse SYMB_MAP_ITEMS

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse Sign

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse Morphism

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse Symbol

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse RAW_SYM

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse where

87a1c79b7b37702a254920ca5214fb282a4fb085dougm basic_analysis LF = Just basicAnalysis

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse stat_symb_items LF _ = symbAnalysis

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse stat_symb_map_items LF _ _ = symbMapAnalysis

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse symbol_to_raw LF = symName

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse matches LF s1 s2 =

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse not (isSym s2) || symName s1 == s2

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse -- expressions are checked manually or symbols match by name

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse empty_signature LF = emptySig

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse is_subsig LF = isSubsig

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse subsig_inclusion LF = inclusionMorph

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse signature_union LF = sigUnion

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse intersection LF = sigIntersection

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse generated_sign LF syms sig = do

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse sig' <- genSig syms sig

87a1c79b7b37702a254920ca5214fb282a4fb085dougm inclusionMorph sig' sig

87a1c79b7b37702a254920ca5214fb282a4fb085dougm cogenerated_sign LF syms sig = do

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse sig' <- coGenSig syms sig

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse inclusionMorph sig' sig

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse induced_from_to_morphism LF m (ExtSign sig1 _) (ExtSign sig2 _) =

87a1c79b7b37702a254920ca5214fb282a4fb085dougm inducedFromToMorphism (translMapAnalysis m sig1 sig2) sig1 sig2

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse induced_from_morphism LF m sig =

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse inducedFromMorphism (renamMapAnalysis m sig) sig

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse

87a1c79b7b37702a254920ca5214fb282a4fb085dougminstance LogicFram LF

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse ()

87a1c79b7b37702a254920ca5214fb282a4fb085dougm BASIC_SPEC

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse Sentence

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse SYMB_ITEMS

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse SYMB_MAP_ITEMS

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse Sign

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse Morphism

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse Symbol

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse RAW_SYM

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse ()

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse where

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse base_sig LF = baseSig

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse write_logic LF = writeLogic

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse write_syntax LF = writeSyntax

03181bdde77be8e10ed297a02db5d8f98ecb703ewrowe write_proof LF = writeProof

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse write_model LF = writeModel

bb0b94431dc9a1591a0a38a6c48925c6d9213c83rse write_comorphism LF = writeComorphism

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse read_morphism LF = readMorphism