Logic_CspCASL.hs revision f08f7774e4c47012f3c349205310750198cdc434
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
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
{- |
Module : $Id$
Description : CspCASL instance of type class logic
Copyright : (c) Markus Roggenbach, Till Mossakowski and Uni Bremen 2003
License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
Maintainer : M.Roggenbach@swansea.ac.uk
Stability : experimental
Portability : non-portable(import Logic.Logic)
Here is the place where the class Logic is instantiated for CspCASL.
Also the instances for Syntax an Category.
-}
{-
todo:
- writing real functions
- Modul Sign.hs mit CSP-CASL-Signaturen und Morphismen, basiernd
auf CASL.Sign
CSP-CASL-Signatur = (CASL-Sig,Menge von Kanalnamen)
CSP-CASL-Morphismus = (CASL-Morphismus, Kanalnamenabbildung)
oder nur CASL-Morphismus
SYMB_ITEMS SYMB_MAP_ITEMS: erstmal von CASL (d.h. nur CASL-Morphismus)
- instance Sentences
S�tze = entweder CASL-S�tze oder CSP-CASL-S�tze
Rest soweit wie m�glich von CASL �bernehmen
- statische Analyse (gem�� Typ in Logic.Logic) schreiben
und unten f�r basic_analysis einh�ngen
K�r:
- Teillogiken (instance SemiLatticeWithTop ...)
-}
module CspCASL.Logic_CspCASL(CspCASL(CspCASL)) where
import Logic.Logic
import CASL.AS_Basic_CASL
import CASL.Logic_CASL
import CASL.Morphism
import CASL.Sign
import CASL.SymbolParser
import CASL.SymbolMapAnalysis
import qualified Data.Set as Set
--import CspCASL.AS_CspCASL
import qualified CspCASL.AS_CspCASL as AS_CspCASL
import qualified CspCASL.ATC_CspCASL()
import qualified CspCASL.CspCASL_Keywords as CspCASL_Keywords
import qualified CspCASL.Morphism as CspCASL_Morphism
import qualified CspCASL.Parse_CspCASL as Parse_CspCASL
import qualified CspCASL.Print_CspCASL ()
import qualified CspCASL.SignCSP as SignCSP
import qualified CspCASL.StatAnaCSP as StatAnaCSP
-- | Lid for CspCASL
data CspCASL = CspCASL deriving (Show)
instance Language CspCASL
where
description _ =
"CspCASL - see\n\n"++
instance SignExtension SignCSP.CspSign where
isSubSignExtension = SignCSP.isInclusion
-- | Instance for CspCASL morphism extension (used for Category)
instance MorphismExtension SignCSP.CspSign SignCSP.CspAddMorphism where
ideMorphismExtension _ = SignCSP.emptyCspAddMorphism
composeMorphismExtension = SignCSP.composeCspAddMorphism
inverseMorphismExtension = SignCSP.inverseCspAddMorphism
isInclusionMorphismExtension _ = True -- missing!
-- | Instance of Sentences for CspCASL (missing)
instance Sentences CspCASL
SignCSP.CspCASLSen -- sentence (missing)
SignCSP.CspCASLSign -- signature
SignCSP.CspMorphism -- morphism
Symbol -- symbol
where
parse_sentence CspCASL = Nothing
map_sen CspCASL mor sen =
if isInclusionMorphism isInclusionMorphismExtension mor
then return sen
else fail "renaming in map_sen CspCASL not implemented"
sym_of CspCASL = CspCASL_Morphism.symOf
symmap_of CspCASL = morphismToSymbMap
-- | Syntax of CspCASL
instance Syntax CspCASL
AS_CspCASL.CspBasicSpec -- basic_spec
SYMB_ITEMS -- symb_items
SYMB_MAP_ITEMS -- symb_map_items
where
parse_basic_spec CspCASL =
parse_symb_items CspCASL =
Just $ symbItems CspCASL_Keywords.csp_casl_keywords
parse_symb_map_items CspCASL =
Just $ symbMapItems CspCASL_Keywords.csp_casl_keywords
-- lattices (for sublogics) missing
-- | Instance of Logic for CspCASL
instance Logic CspCASL
() -- Sublogics (missing)
AS_CspCASL.CspBasicSpec -- basic_spec
SignCSP.CspCASLSen -- sentence (missing)
SYMB_ITEMS -- symb_items
SYMB_MAP_ITEMS -- symb_map_items
SignCSP.CspCASLSign -- signature
SignCSP.CspMorphism -- morphism
Symbol
RawSymbol
() -- proof_tree (missing)
where
stability CspCASL = Experimental
data_logic CspCASL = Just (Logic CASL)
empty_proof_tree _ = ()
-- | Static Analysis for CspCASL
instance StaticAnalysis CspCASL
AS_CspCASL.CspBasicSpec -- basic_spec
SignCSP.CspCASLSen -- sentence (missing)
SYMB_ITEMS -- symb_items
SYMB_MAP_ITEMS -- symb_map_items
SignCSP.CspCASLSign -- signature
SignCSP.CspMorphism -- morphism
Symbol
RawSymbol
where
basic_analysis CspCASL =
stat_symb_map_items CspCASL = error "Logic_CspCASL.hs"
stat_symb_items CspCASL = error "Logic_CspCASL.hs"
empty_signature CspCASL = SignCSP.emptyCspCASLSign
inclusion CspCASL =
sigInclusion SignCSP.emptyCspAddMorphism
SignCSP.isInclusion const -- this is still wrong
signature_union CspCASL s =
return . addSig SignCSP.addCspProcSig s
induced_from_morphism CspCASL = inducedFromMorphism
induced_from_to_morphism CspCASL = inducedFromToMorphism