hets/LF/Logic_LF.hs

	Logic_LF.hs revision d2786879b4733fd4886a5b654f7c6de1d234f638
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner{- |
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillyModule      :  $Header$
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillyDescription :  Instances of classes defined in Logic.hs for the Edinburgh
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly               Logical Framework
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillyLicense     :  GPLv2 or higher, see LICENSE.txt
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillyMaintainer  :  k.sojakova@jacobs-university.de
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillyStability   :  experimental
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillyPortability :  portable
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly-}
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reillymodule LF.Logic_LF where
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reillyimport LF.AS
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reillyimport LF.Parse
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reillyimport LF.Sign
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reillyimport LF.Morphism
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reillyimport LF.ATC_LF ()
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reillyimport LF.Analysis
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reillyimport LF.Framework
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reillyimport Logic.Logic
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reillyimport Common.Result
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reillyimport qualified Data.Map as Map
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillydata LF = LF deriving Show
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reillyinstance Language LF where
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   description LF = "Edinburgh Logical Framework"
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reillyinstance Category Sign Morphism where
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   ide = idMorph
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly   dom = source
1b2195930f52ad43e6bb64b1df0cf6718bfd84c0Liam O'Reilly   cod = target
1b2195930f52ad43e6bb64b1df0cf6718bfd84c0Liam O'Reilly   composeMorphisms = compMorph
1b2195930f52ad43e6bb64b1df0cf6718bfd84c0Liam O'Reilly   isInclusion = Map.null . symMap . canForm
1b2195930f52ad43e6bb64b1df0cf6718bfd84c0Liam O'Reilly   legal_mor = const True
1b2195930f52ad43e6bb64b1df0cf6718bfd84c0Liam O'Reilly
1b2195930f52ad43e6bb64b1df0cf6718bfd84c0Liam O'Reillyinstance Syntax LF BASIC_SPEC SYMB_ITEMS SYMB_MAP_ITEMS where
1b2195930f52ad43e6bb64b1df0cf6718bfd84c0Liam O'Reilly   parse_basic_spec LF = Just basicSpec
1b2195930f52ad43e6bb64b1df0cf6718bfd84c0Liam O'Reilly   parse_symb_items LF = Just symbItems
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   parse_symb_map_items LF = Just symbMapItems
9738b4e358f960105062839c835bb9eff3e44588Liam O'Reilly
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reillyinstance Sentences LF
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly   Sentence
9738b4e358f960105062839c835bb9eff3e44588Liam O'Reilly   Sign
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   Morphism
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly   Symbol
9738b4e358f960105062839c835bb9eff3e44588Liam O'Reilly   where
9738b4e358f960105062839c835bb9eff3e44588Liam O'Reilly   map_sen LF m = (Result []) . (translate m)
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   sym_of LF = singletonList . getSymbols
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance Logic LF
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   ()
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   BASIC_SPEC
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   Sentence
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   SYMB_ITEMS
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   SYMB_MAP_ITEMS
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   Sign
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   Morphism
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   Symbol
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   Symbol
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   ()
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reillyinstance StaticAnalysis LF
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly   BASIC_SPEC
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly   Sentence
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly   SYMB_ITEMS
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder   SYMB_MAP_ITEMS
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   Sign
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder   Morphism
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder   Symbol
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly   Symbol
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly   where
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   basic_analysis LF = Just $ basicAnalysis
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   empty_signature LF = emptySig
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly   signature_union LF = sigUnion
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly   is_subsig LF = isSubsig
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   subsig_inclusion LF = inclusionMorph
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reillyinstance LogicFram LF
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder   ()
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly   BASIC_SPEC
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly   Sentence
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   SYMB_ITEMS
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   SYMB_MAP_ITEMS
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   Sign
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder   Morphism
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder   Symbol
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   Symbol
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   ()
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly   where
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly   getBaseSig LF = baseSigLF
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   writeLogic LF = writeLogicLF
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly   writeSyntax LF = writeSyntaxLF
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly