Grothendieck.hs revision 6f3198a56c02c18d02d19b4aaad1c395686aec07
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
-- needs ghc -fglasgow-exts
$Id$
Till Mossakowski
The Grothendieck logic is defined to be the
heterogeneous logic over the logic graph.
This will be the logic over which the data
structures and algorithms for specification in-the-large
are built.
References:
R. Diaconescu:
Grothendieck institutions
J. applied categorical structures, to appear
T. Mossakowski:
Heterogeneous development graphs and heterogeneous borrowing
Fossacs 2002, LNCS 2303
T. Mossakowski: Simplified heterogeneous specification
Submitted
Todo:
-}
module Grothendieck where
import Logic
import LogicGraph
import Dynamic
data Grothendieck = Grothendieck
data G_basic_spec = forall id sublogics
basic_spec sentence symb_items symb_map_items
local_env sign morphism symbol raw_symbol .
Logic id sublogics
basic_spec sentence symb_items symb_map_items
local_env sign morphism symbol raw_symbol =>
G_basic_spec id basic_spec
data G_sentence = forall id sublogics
basic_spec sentence symb_items symb_map_items
local_env sign morphism symbol raw_symbol .
Logic id sublogics
basic_spec sentence symb_items symb_map_items
local_env sign morphism symbol raw_symbol =>
G_sentence id sentence
data G_sign = forall id sublogics
basic_spec sentence symb_items symb_map_items
local_env sign morphism symbol raw_symbol .
Logic id sublogics
basic_spec sentence symb_items symb_map_items
local_env sign morphism symbol raw_symbol =>
G_sign id sign
data G_morphism = forall id sublogics
basic_spec sentence symb_items symb_map_items
local_env sign morphism symbol raw_symbol .
Logic id sublogics
basic_spec sentence symb_items symb_map_items
local_env sign morphism symbol raw_symbol =>
G_morphism id morphism
data G_symbol = forall id sublogics
basic_spec sentence symb_items symb_map_items
local_env sign morphism symbol raw_symbol .
Logic id sublogics
basic_spec sentence symb_items symb_map_items
local_env sign morphism symbol raw_symbol =>
G_symbol id symbol
data G_symb_items = forall id sublogics
basic_spec sentence symb_items symb_map_items
local_env sign morphism symbol raw_symbol .
Logic id sublogics
basic_spec sentence symb_items symb_map_items
local_env sign morphism symbol raw_symbol =>
G_symb_items id symb_items
data G_symb_items_list = forall id sublogics
basic_spec sentence symb_items symb_map_items
local_env sign morphism symbol raw_symbol .
Logic id sublogics
basic_spec sentence symb_items symb_map_items
local_env sign morphism symbol raw_symbol =>
G_symb_items_list id [symb_items]
data G_symb_map_items = forall id sublogics
basic_spec sentence symb_items symb_map_items
local_env sign morphism symbol raw_symbol .
Logic id sublogics
basic_spec sentence symb_items symb_map_items
local_env sign morphism symbol raw_symbol =>
G_symb_map_items id symb_map_items
coerce :: a -> Maybe b = fromDynamic . toDyn
homogenize_symb_items :: [G_symb_items] -> Maybe G_symb_items_list
homogenize_symb_items [] = Nothing
homogenize_symb_items (G_symb_items i (s::symb_map_items) : rest) =
maybe Nothing
(\l -> Just (G_symb_items_list i l))
( sequence (Just s :
map (\(G_symb_items _ si) -> coerce si::Maybe symb_map_items) rest) )