{-# 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 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 _ = "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 = 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