hets/LF/Logic_LF.hs

	Logic_LF.hs revision 80d2ec8f37d5ddec13c14b17b1bab01e9c94630a
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy{- |
f38cb554a534c6df738be3f4d23327e69888e634John Wren KennedyModule      :  $Header$
f38cb554a534c6df738be3f4d23327e69888e634John Wren KennedyDescription :  Instances of classes defined in Logic.hs for the Edinburgh
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy               Logical Framework
f38cb554a534c6df738be3f4d23327e69888e634John Wren KennedyCopyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
f38cb554a534c6df738be3f4d23327e69888e634John Wren KennedyLicense     :  GPLv2 or higher, see LICENSE.txt
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy
f38cb554a534c6df738be3f4d23327e69888e634John Wren KennedyMaintainer  :  k.sojakova@jacobs-university.de
f38cb554a534c6df738be3f4d23327e69888e634John Wren KennedyStability   :  experimental
f38cb554a534c6df738be3f4d23327e69888e634John Wren KennedyPortability :  portable
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy-}
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedymodule LF.Logic_LF where
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedyimport LF.AS
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedyimport LF.Parse
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedyimport LF.Sign
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedyimport LF.Morphism
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedyimport LF.ATC_LF ()
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedyimport LF.Analysis
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedyimport LF.Framework
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedyimport Logic.Logic
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedyimport Common.Result
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedyimport Common.ExtSign
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy
1d32ba663e202c24a5a1f2e5aef83fffb447cb7fJohn Wren Kennedyimport qualified Data.Map as Map
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedydata LF = LF deriving Show
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedyinstance Language LF where
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   description LF = "Edinburgh Logical Framework"
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedyinstance Category Sign Morphism where
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   ide = idMorph
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   dom = source
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   cod = target
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   composeMorphisms = compMorph
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   isInclusion = Map.null . symMap . canForm
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   legal_mor = const True
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedyinstance Syntax LF BASIC_SPEC SYMB_ITEMS SYMB_MAP_ITEMS where
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   parse_basic_spec LF = Just basicSpec
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   parse_symb_items LF = Just symbItems
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   parse_symb_map_items LF = Just symbMapItems
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedyinstance Sentences LF
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   Sentence
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   Sign
1d32ba663e202c24a5a1f2e5aef83fffb447cb7fJohn Wren Kennedy   Morphism
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   Symbol
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   where
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   map_sen LF m = (Result []) . (translate m)
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   sym_of LF = singletonList . getSymbols
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedyinstance Logic LF
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   ()
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   BASIC_SPEC
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   Sentence
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   SYMB_ITEMS
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   SYMB_MAP_ITEMS
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   Sign
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   Morphism
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   Symbol
1d32ba663e202c24a5a1f2e5aef83fffb447cb7fJohn Wren Kennedy   RAW_SYM
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   ()
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedyinstance StaticAnalysis LF
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   BASIC_SPEC
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   Sentence
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   SYMB_ITEMS
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   SYMB_MAP_ITEMS
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   Sign
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   Morphism
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   Symbol
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   RAW_SYM
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   where
f38cb554a534c6df738be3f4d23327e69888e634John Wren Kennedy   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 =
     if (isSym s2)
        then symName s1 == s2         --symbols are matched by their name
        else True   -- expressions are checked manually hence always True
   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