-
Notifications
You must be signed in to change notification settings - Fork 19
/
Copy pathToItem.hs
199 lines (157 loc) · 7.34 KB
/
ToItem.hs
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
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module : $Header$
Description : extracted annotated items as strings from BASIC_SPEC
Copyright : (c) Christian Maeder and Ewaryst Schulz and DFKI GmbH 2009
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Ewaryst.Schulz@dfki.de
Stability : experimental
Portability : non-portable
get item representation of 'BASIC_SPEC'
-}
module CASL.ToItem (bsToItem) where
import Control.Monad.Reader
import Common.Doc
import Common.DocUtils
import Common.Id
import Common.Item
import CASL.AS_Basic_CASL
import CASL.ToDoc
--------------------- TS = TransState
data TS b s f = TS { fB :: b -> Doc
, fS :: s -> Doc }
-- LITC = LocalITContext
-- This datastructure is used to pass an additional ItemType argument to
-- the toitem method when one needs an instance for which this method
-- should behave differently in different contexts depending on this argument.
-- Typically the ItemType is used as ItemType of the Item to be created.
data LITC a = LITC ItemType a
--------------------- lifting to Local Contexts
withLIT :: ItemTypeable a => a -> b -> LITC b
withLIT = LITC . toIT
listWithLIT :: ItemTypeable a => a -> [b] -> [LITC b]
listWithLIT = map . withLIT
-- analogous for annotated objects, don't needed yet
--annWithLIT :: ItemTypeable a => a -> Annoted b -> Annoted (LITC b)
--annWithLIT it = fmap (withLIT it)
--annlistWithLIT :: ItemTypeable a => a -> [Annoted b] -> [Annoted (LITC b)]
--annlistWithLIT it = map (annWithLIT it)
-- this function is only to unify the types of the state and the basic spec
-- in the call of toitem and runState in bsToItem
getTransState :: (Pretty b, Pretty s)
=> BASIC_SPEC b s f -> TS b s f
getTransState _ = TS pretty pretty
--------------------- The Main function of this module
bsToItem :: (Pretty b, Pretty s, GetRange b, GetRange s, FormExtension f)
=> BASIC_SPEC b s f -> Item
bsToItem bs = runReader (toitem bs) $ getTransState bs
instance (GetRange b, GetRange s, FormExtension f)
=> ItemConvertible (BASIC_SPEC b s f) (Reader (TS b s f)) where
toitem (Basic_spec l) = do
l' <- listFromAL l
return rootItem { items = l' }
instance (GetRange b, GetRange s, FormExtension f)
=> ItemConvertible (BASIC_ITEMS b s f) (Reader (TS b s f)) where
toitem bi = let rg = getRangeSpan bi in
case bi of
Sig_items s -> toitem s
Var_items l _ -> mkItemM "Var_items" rg $ listFromL l
Axiom_items al _ -> mkItemM "Axiom_items" rg $ listFromAL al
Local_var_axioms vl fl _ ->
mkItemMM "Local_var_axioms" rg
[fromL "VAR_DECLS" vl, fromAL "FORMULAS" fl]
Sort_gen asis _ -> mkItemM "Sort_gen" rg $ listFromAL asis
Free_datatype sk adtds _ ->
mkItemM ("Free_datatype", "SortsKind", show sk) rg
$ listFromAL adtds
Ext_BASIC_ITEMS b -> do
st <- ask
fromPrinter (fB st) "Ext_BASIC_ITEMS" b
instance (GetRange s, FormExtension f)
=> ItemConvertible (SIG_ITEMS s f) (Reader (TS b s f)) where
toitem si = let rg = getRangeSpan si in
case si of
Sort_items sk sis _ ->
mkItemM ("Sort_items", "SortsKind", show sk) rg
$ listFromAL sis
Op_items aois _ -> mkItemM "Op_items" rg $ listFromAL aois
Pred_items apis _ -> mkItemM "Pred_items" rg $ listFromAL apis
Datatype_items sk adds _ ->
mkItemM ("Datatype_items", "SortsKind", show sk) rg
$ listFromAL adds
Ext_SIG_ITEMS s -> do
st <- ask
fromPrinter (fS st) "Ext_SIG_ITEMS" s
instance FormExtension f
=> ItemConvertible (SORT_ITEM f) (Reader (TS b s f)) where
toitem si = let rg = getRangeSpan si in
case si of
Sort_decl l _ -> mkItemM "Sort_decl" rg $ listFromL
$ listWithLIT "SORT" l
Subsort_decl sl s _ -> mkItemMM "Subsort_decl" rg
[ fromL "SORTS" $ listWithLIT "SORT" sl
, fromC $ withLIT "SORT" s]
Subsort_defn s v s' f _ ->
mkItemMM "Subsort_defn" rg
[ fromC $ withLIT "SORT" s, fromC $ withLIT "VAR" v
, fromC $ withLIT "SORT" s', fromAC f]
Iso_decl l _ -> mkItemM "Iso_decl" rg $ listFromL
$ listWithLIT "SORT" l
instance FormExtension f
=> ItemConvertible (OP_ITEM f) (Reader (TS b s f)) where
toitem oi = let rg = getRangeSpan oi in
case oi of
Op_decl onl ot oal _ ->
mkItemMM "Op_decl" rg
[ fromL "OP_NAMES" $ listWithLIT "OP_NAME" onl, fromC ot
, fromL "OP_ATTRIBS" oal]
Op_defn on oh at _ ->
mkItemMM "Op_defn" rg [ fromC $ withLIT "OP_NAME" on, fromC oh
, fromAC at]
instance FormExtension f
=> ItemConvertible (PRED_ITEM f) (Reader (TS b s f)) where
toitem p = let rg = getRangeSpan p in
case p of
Pred_decl pnl pt _ ->
mkItemMM "Pred_decl" rg
[fromL "PRED_NAMES" $ listWithLIT "PRED_NAME" pnl, fromC pt]
Pred_defn pn ph af _ ->
mkItemMM "Pred_defn" rg [ fromC $ withLIT "PRED_NAME" pn, fromC ph
, fromAC af]
-------------------- not further expanded --------------------
fromPrinterWithRg :: (Monad m, GetRange a) =>
(a -> Doc) -> String -> a -> m Item
fromPrinterWithRg = fromPrinterWithRange getRangeSpan
fromPrinterWithRange
:: Monad m => (a -> Range) -> (a -> Doc) -> String -> a -> m Item
fromPrinterWithRange r p n o = mkItemMM (n, p o) (r o) []
fromPrinter :: Monad m => (a -> Doc) -> String -> a -> m Item
fromPrinter p n o = mkItemMM (n, p o) nullRange []
litFromPrinterWithRg :: (Monad m, GetRange a) =>
(a -> Doc) -> LITC a -> m Item
litFromPrinterWithRg p (LITC (IT l attrs _) o) =
mkItemMM (IT l attrs $ Just $ p o) (getRangeSpan o) []
instance ItemConvertible OP_TYPE (Reader (TS b s f)) where
toitem = fromPrinterWithRg pretty "OP_TYPE"
instance ItemConvertible OP_HEAD (Reader (TS b s f)) where
toitem = fromPrinterWithRg pretty "OP_HEAD"
instance FormExtension f
=> ItemConvertible (OP_ATTR f) (Reader (TS b s f)) where
toitem = fromPrinter printAttr "OP_ATTR"
instance ItemConvertible PRED_TYPE (Reader (TS b s f)) where
toitem = fromPrinterWithRg pretty "PRED_TYPE"
instance ItemConvertible PRED_HEAD (Reader (TS b s f)) where
toitem = fromPrinterWithRg printPredHead "PRED_HEAD"
instance ItemConvertible DATATYPE_DECL (Reader (TS b s f)) where
toitem = fromPrinterWithRg pretty "DATATYPE_DECL"
instance ItemConvertible VAR_DECL (Reader (TS b s f)) where
toitem = fromPrinterWithRg pretty "VAR_DECL"
instance FormExtension f
=> ItemConvertible (FORMULA f) (Reader (TS b s f)) where
toitem = fromPrinterWithRange getRangeSpan printFormula "FORMULA"
instance FormExtension f => ItemConvertible (TERM f) (Reader (TS b s f)) where
toitem = fromPrinterWithRange getRangeSpan printTerm "TERM"
instance ItemConvertible (LITC Id) (Reader (TS b s f)) where
toitem = litFromPrinterWithRg pretty
instance ItemConvertible (LITC Token) (Reader (TS b s f)) where
toitem = litFromPrinterWithRg pretty