hets/LF/Logic_LF.hs

	Logic_LF.hs revision e16b3696b2c173aac14200321868ed81b8f7dc69
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder{- |
f0cb315452faea6fee8144489629e63e9bd7b303Christian MaederModule      :  $Header$
f0cb315452faea6fee8144489629e63e9bd7b303Christian MaederDescription :  Instances of classes defined in Logic.hs for the Edinburgh
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder               Logical Framework
f0cb315452faea6fee8144489629e63e9bd7b303Christian MaederCopyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
f0cb315452faea6fee8144489629e63e9bd7b303Christian MaederLicense     :  GPLv2 or higher, see LICENSE.txt
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder
f0cb315452faea6fee8144489629e63e9bd7b303Christian MaederMaintainer  :  k.sojakova@jacobs-university.de
f0cb315452faea6fee8144489629e63e9bd7b303Christian MaederStability   :  experimental
f0cb315452faea6fee8144489629e63e9bd7b303Christian MaederPortability :  portable
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder-}
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maedermodule LF.Logic_LF where
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederimport LF.AS
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederimport LF.Parse
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederimport LF.MorphParser (readMorphism)
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederimport LF.Sign
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederimport LF.Morphism
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederimport LF.ATC_LF ()
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederimport LF.Analysis
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederimport LF.Framework
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederimport LF.ComorphFram ()
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederimport Logic.Logic
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederimport Common.Result
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederimport Common.ExtSign
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederimport qualified Data.Map as Map
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederimport Data.Monoid
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederdata LF = LF deriving Show
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederinstance Language LF where
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder   description LF = "Edinburgh Logical Framework"
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederinstance Category Sign Morphism where
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder   ide = idMorph
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder   dom = source
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder   cod = target
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder   composeMorphisms = compMorph
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder   isInclusion = Map.null . symMap . canForm
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederinstance Monoid BASIC_SPEC where
41582f75931338095dc749c455593c859376d593Christian Maeder    mempty = Basic_spec []
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder    mappend (Basic_spec l1) (Basic_spec l2) = Basic_spec $ l1 ++ l2
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederinstance Syntax LF BASIC_SPEC SYMB_ITEMS SYMB_MAP_ITEMS where
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder   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

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 LogicFram 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