2d0611ffc9f91c5fc2ddccb93f9a3d17791ae650takashi{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

2d0611ffc9f91c5fc2ddccb93f9a3d17791ae650takashi{- |

dc0d8d65d35787d30a275895ccad8d8e1b58a5edndModule : ./LF/Logic_LF.hs

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

dc0d8d65d35787d30a275895ccad8d8e1b58a5ednd Logical Framework

dc0d8d65d35787d30a275895ccad8d8e1b58a5edndCopyright : (c) Kristina Sojakova, DFKI Bremen 2009

dc0d8d65d35787d30a275895ccad8d8e1b58a5edndLicense : GPLv2 or higher, see LICENSE.txt

dc0d8d65d35787d30a275895ccad8d8e1b58a5ednd

dc0d8d65d35787d30a275895ccad8d8e1b58a5edndMaintainer : k.sojakova@jacobs-university.de

dc0d8d65d35787d30a275895ccad8d8e1b58a5edndStability : experimental

6ae232055d4d8a97267517c5e50074c2c819941andPortability : portable

dc0d8d65d35787d30a275895ccad8d8e1b58a5ednd-}

6ae232055d4d8a97267517c5e50074c2c819941and

e1e8390280254f7f0580d701e583f670643d4f3fnilgunmodule LF.Logic_LF where

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunimport LF.AS

e1e8390280254f7f0580d701e583f670643d4f3fnilgunimport 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 Show

instance Language LF where

description LF = "Edinburgh Logical Framework"

instance Category Sign Morphism where

ide = idMorph

dom = source

cod = target

composeMorphisms = compMorph

isInclusion = Map.null . symMap . canForm

instance Monoid BASIC_SPEC where

mempty = Basic_spec []

mappend (Basic_spec l1) (Basic_spec l2) = Basic_spec $ l1 ++ l2

instance Syntax LF BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS where

parse_basic_spec LF = Just basicSpec

parse_symb_items LF = Just symbItems

parse_symb_map_items LF = Just symbMapItems

instance Sentences LF

Sentence

Sign

Morphism

Symbol

where

map_sen LF m = Result [] . translate m

sym_of LF = singletonList . getSymbols

symKind LF _ = "op"

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 = Just basicAnalysis

stat_symb_items LF _ = symbAnalysis

stat_symb_map_items LF _ _ = symbMapAnalysis

symbol_to_raw LF = symName

matches LF s1 s2 =

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

-- expressions are checked manually or symbols match by name

empty_signature LF = emptySig

is_subsig LF = isSubsig

subsig_inclusion LF = inclusionMorph

signature_union LF = sigUnion

intersection LF = sigIntersection

generated_sign LF syms sig = do

sig' <- genSig syms sig

inclusionMorph sig' sig

cogenerated_sign LF syms sig = do

sig' <- coGenSig syms sig

inclusionMorph sig' sig

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

inducedFromToMorphism (translMapAnalysis m sig1 sig2) sig1 sig2

induced_from_morphism LF m sig =

inducedFromMorphism (renamMapAnalysis m sig) sig

instance LogicalFramework LF

()

BASIC_SPEC

Sentence

SYMB_ITEMS

SYMB_MAP_ITEMS

Sign

Morphism

Symbol

RAW_SYM

()

where

base_sig LF = baseSig

write_logic LF = writeLogic

write_syntax LF = writeSyntax

write_proof LF = writeProof

write_model LF = writeModel

write_comorphism LF = writeComorphism

read_morphism LF = readMorphism