hets/LF/Logic_LF.hs

	Logic_LF.hs revision 80d2ec8f37d5ddec13c14b17b1bab01e9c94630a


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
{- |
Module      :  $Header$
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.Sign
import LF.Morphism
import LF.ATC_LF ()
import LF.Analysis
import LF.Framework

import Logic.Logic

import Common.Result
import Common.ExtSign

import qualified Data.Map as Map

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
   legal_mor = const True

instance Syntax LF BASIC_SPEC 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

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