hets/CASL/Logic_CASL.hs

	Logic_CASL.hs revision 3b4439aa37e4229ad6e83d46bd303c2799784c80


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
152
{-# OPTIONS -fno-warn-missing-methods #-}
{- HetCATS/CASL/Logic_CASL.hs
   $Id$
   Authors: Klaus L�ttich
   Year:    2002

   Here is the place where the class Logic is instantiated for CASL.
   Also the instances for Syntax an Category.

   todo:
     - writing real functions

-}

module Logic_CASL where

import AS_Basic_CASL
import Print_AS_Basic
import Parse_AS_Basic
import SymbolParser
import ParsecInterface
import AnnoState(emptyAnnos)

import Sign
import Logic

import qualified Sublogics
import qualified Static

-- a dummy datatype for the LogicGraph and for identifying the right
-- instances
data CASL = CASL deriving (Show)
instance Language CASL where  -- default definition is okay

instance Category CASL Sign Morphism
    where
         -- ide :: id -> object -> morphism
     ide CASL sigma = Morphism { msource = sigma,
                                     mtarget = sigma
                                   }
         -- o :: id -> morphism -> morphism -> Maybe morphism
     comp CASL sigma1 sigma2 = Just sigma1 -- ???
         -- dom, cod :: id -> morphism -> object
     dom CASL _ = emptySign
     cod CASL _ = emptySign
         -- legal_obj :: id -> object -> Bool
     legal_obj CASL _ = fun_err "legall_obj"
         -- legal_mor :: id -> morphism -> Bool
     legal_mor CASL _ = fun_err "legal_mor"


-- abstract syntax, parsing (and printing)

instance Syntax CASL BASIC_SPEC
        SYMB_ITEMS SYMB_MAP_ITEMS
      where
         parse_basic_spec CASL = Just(toParseFun basicSpec emptyAnnos)
     parse_symb_items CASL = Just(toParseFun symbItems ())
     parse_symb_map_items CASL = Just(toParseFun symbMapItems ())

-- lattices (for sublogics)

instance LatticeWithTop Sublogics.CASL_Sublogics where
    -- meet, join :: l -> l -> l
    meet = Sublogics.sublogics_min
    join = Sublogics.sublogics_max
    -- top :: l
    top = Sublogics.top

-- CASL logic

instance Sentences CASL Sentence Sign Morphism Symbol where
-- missing

instance StaticAnalysis CASL BASIC_SPEC Sentence
               SYMB_ITEMS SYMB_MAP_ITEMS
               Sign
               Morphism
               Symbol RawSymbol where
         basic_analysis CASL = Just Static.basicAnalysis
         stat_symb_map_items CASL = Static.statSymbMapItems
         stat_symb_items CASL = Static.statSymbItems
         -- ensures_amalgamability :: id
         --   -> (Diagram Sign Morphism, Node, Sign, LEdge Morphism, Morphism)
         --   -> Result (Diagram Sign Morphism)

         sign_to_basic_spec CASL sigma sens = Basic_spec []

         symbol_to_raw CASL = Static.symbolToRaw
         id_to_raw CASL = Static.idToRaw
         sym_of CASL = Static.symOf
         symmap_of CASL = Static.symmapOf
         matches CASL = Static.matches
         sym_name CASL = Static.symName

         -- add_sign :: id -> Sign -> Sign -> Sign
         empty_signature CASL = emptySign
         signature_union CASL sigma1 sigma2 = return sigma1 -- ??? incorrect
         morphism_union CASL mor1 mor2 = return mor1 -- ??? incorrect
         -- final_union :: id -> Sign -> Sign -> Result Sign
         is_subsig CASL = Static.isSubSig
         cogenerated_sign CASL rsys sigma = return (ide CASL sigma)
         generated_sign CASL rsys sigma = return (ide CASL sigma)
         -- generated_sign, cogenerated_sign :: id -> [RawSymbol]
         --                -> Sign -> Result Morphism
         induced_from_morphism CASL rmap sigma = return (ide CASL sigma) -- ???
         induced_from_to_morphism CASL rmap sigmaS sigmaT =
           return (ide CASL sigmaS) -- ???
         --induced_from_to_morphism :: id -> EndoMap RawSymbol
         --               -> Sign -> Sign -> Result Morphism
         -- extend_morphism :: id -> Sign -> Morphism -> Sign -> Sign
         --               -> Result Morphism

instance Logic CASL Sublogics.CASL_Sublogics
               BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS
               Sign
               Morphism
               Symbol RawSymbol where
         sublogic_names CASL = Sublogics.sublogics_name
         all_sublogics CASL = Sublogics.sublogics_all

         is_in_basic_spec CASL = Sublogics.in_basic_spec
         is_in_sentence CASL = Sublogics.in_sentence
         is_in_symb_items CASL = Sublogics.in_symb_items
         is_in_symb_map_items CASL = Sublogics.in_symb_map_items
         is_in_sign CASL = Sublogics.in_sign
         is_in_morphism CASL = Sublogics.in_morphism
         is_in_symbol CASL = Sublogics.in_symbol

         min_sublogic_basic_spec CASL = Sublogics.sl_basic_spec
         min_sublogic_sentence CASL = Sublogics.sl_sentence
         min_sublogic_symb_items CASL = Sublogics.sl_symb_items
         min_sublogic_symb_map_items CASL = Sublogics.sl_symb_map_items
         min_sublogic_sign CASL = Sublogics.sl_sign
         min_sublogic_morphism CASL = Sublogics.sl_morphism
         min_sublogic_symbol CASL = Sublogics.sl_symbol

         proj_sublogic_basic_spec CASL = Sublogics.pr_basic_spec
         proj_sublogic_symb_items CASL = Sublogics.pr_symb_items
         proj_sublogic_symb_map_items CASL = Sublogics.pr_symb_map_items
         proj_sublogic_sign CASL = Sublogics.pr_sign
         proj_sublogic_morphism CASL = Sublogics.pr_morphism
         proj_sublogic_epsilon CASL = Sublogics.pr_epsilon
         proj_sublogic_symbol CASL = Sublogics.pr_symbol

---- helpers ---------------------------------
fun_err :: String -> a
fun_err fname =
    error ("*** Function \"" ++ fname ++ "\" is not yet implemented!")

----------------------------------------------