[project @ 1996-01-08 20:13:28 by partain]
[nofib.git] / real / veritas / Display.hs
1 module Display where
2
3 import Core_datatype
4
5 import Edlib
6
7 import X_interface
8
9 import Kernel
10
11 import Parse
12
13 import Unparse
14
15 import Vtslib
16
17 import Type_defs
18
19 import Lookup
20
21 import Globals
22
23 import Tags
24
25 import Goals
26
27 import Tree
28
29
30 typeL = ["Thm","Trm","Sgn","Dec"]
31
32
33 wins = ["Own","Scratch"]
34
35
36
37 select :: (Eq b) => b -> [b] -> Int
38
39 select s [] = 0
40
41 select s (s' : l) = if s==s' then 0 else 1+select s l
42
43
44
45 make_form ty sp win err
46 = [
47 InComment " Parse Object",
48 InRadio "Type of Object"
49 (case ty of
50 SOME x -> select x typeL
51 _ -> 0 )
52 typeL ,
53 InComment "",
54 InMultiText "Specification"
55 ( case sp of
56 SOME x -> x
57 _ -> "" ),
58 InRadio "Display Window"
59 ( case win of
60 SOME x -> select x wins
61 _ -> 0 )
62 wins
63 ] ++
64 (case err of
65 SOME err' -> [InComment err']
66 _ -> [])
67
68 {-
69 unerr (Unbound s) = "Unbound symbol " ^ s
70
71 unerr (UnboundRec s) = "Unbound rec symbol " ^ s
72
73 unerr NonAtomic = "Not atomic"
74
75 unerr (NonInfixBinder s) = "Expected infixbinder, found " ^ s
76
77 unerr (NonNumber s) = "Not a number " ^ s
78
79 unerr (Reserved s) = "Unexpected reserved word " ^ s
80
81 unerr OtherError = "Syntax error"
82 -}
83
84 --eexperr t1 t2 = "Expected "^t1^" but found "^t2
85
86
87 theory_form = [
88 InComment " Show Theory",
89 InRadio "Display Theory" 1 ["Strcutured","Unstructered",
90 "Just Names"]
91 ]
92
93
94
95
96 show_goal_cmd tr@(TreeSt t _ gst)
97 = x_display title display ./.
98 return tr
99 where
100 title = (case obj of
101 ThmSpec _ -> "Thm Goal No: "
102 TrmSpec _ -> "Trm Goal No: "
103 SgnSpec _ -> "Sgn Goal No: "
104 DecSpec _ -> "Dec Goal No: " )
105 ++ uid
106 display = unparse_obj sg gst obj
107 (Tree (Goal _ _ _ uid obj _ sg _) _ _ _ _ ) = t
108
109
110
111 show_subgoal_cmd :: Int -> (Tree_state GOAL b (c, d, e)) -> Xin
112 -> Xst ( Maybe (Tree_state GOAL b (c, d, e)) f )
113
114 show_subgoal_cmd i tr@( TreeSt (Tree _ tl _ _ _) _ gst)
115 = x_display title display ./.
116 return tr
117 where
118 title = ( case obj of
119 ThmSpec _ -> "Thm Goal No: "
120 TrmSpec _ -> "Trm Goal No: "
121 SgnSpec _ -> "Sgn Goal No: "
122 DecSpec _ -> "Dec Goal No: " )
123 ++ uid
124 display = unparse_obj sg gst obj
125 ( Tree (Goal _ _ _ uid obj _ sg _) _ _ _ _ ) = tl !! i
126
127
128
129 show_theory tr@( TreeSt (Tree g _ _ _ _) _ gst)
130 = x_form True theory_form /./
131 disp
132 where
133 disp ( SOME [(OutRadio "Strcutured")] )
134 = show_theory' tr (unparse_Sgn (error "") (get_attributes gst)) g
135 disp ( SOME [(OutRadio "Unstructered")] )
136 = show_theory' tr display_Sgn g
137 disp ( SOME [(OutRadio "Just Names")] )
138 = show_theory' tr summary_Sgn g
139 disp _ = return tr
140
141 display_Sgn = error "unimplemented in display"
142 summary_Sgn = error "unimplemented in display"
143
144
145
146
147
148
149 show_theory' tr unparse_fn (Goal _ _ _ uid _ True sg lt)
150 = x_display title display ./.
151 return tr
152 where
153 title = "Signature of Node No. " ++ uid
154 display = unparse_fn sg
155
156 show_theory' tr unparse_fn (Goal _ _ _ _ _ False _ _)
157 = x_set_status "Theory not yet defined" ./.
158 return tr
159
160
161
162
163
164 show_object tr@( TreeSt (Tree g _ _ _ _) _ gst)
165 = case g of
166 Goal _ _ _ uid _ True sg lt
167 -> show_obj sg gst' sg att NONE NONE NONE NONE /./
168 ( \ _ -> return tr )
169 where
170 -- gst' = get_default_ps gst
171 gst' = gst -- find get_default_ps
172 att = get_attributes gst
173 Goal _ _ _ _ _ False _ _
174 -> x_set_status "Theory not yet defined" ./.
175 return tr
176
177
178
179
180 show_com t@(Tree (Goal _ _ (SOME com) uid _ _ _ _) _ _ _ _)
181 = x_display ("Comment for Node No: " ++ uid) com ./.
182 return t
183
184 show_com t@(Tree (Goal _ _ NONE _ _ _ _ _) _ _ _ _)
185 = x_set_status "No Comment defined" ./.
186 return t
187
188
189 get_comment (Tree (Goal _ _ NONE _ _ _ _ _) _ _ _ _) = ""
190
191 get_comment (Tree (Goal _ _ (SOME s) _ _ _ _ _) _ _ _ _) = s
192
193
194
195
196 set_comment "" (Tree (Goal a b _ d e f g h) i j k l)
197 = Tree (Goal a b NONE d e f g h) i j k l
198
199 set_comment c (Tree (Goal a b _ d e f g h) i j k l)
200 = Tree (Goal a b (SOME c) d e f g h) i j k l
201
202
203
204
205 unparse_obj sg gst (TrmSpec tm)
206 = unparse_trm sg (get_attributes gst) tm
207
208 unparse_obj sg gst (ThmSpec tm)
209 = unparse_trm sg (get_attributes gst) tm
210
211 unparse_obj sg gst (DecSpec dc)
212 = unparse_dec sg (get_attributes gst) dc
213
214 unparse_obj sg gst (SgnSpec isg)
215 = unparse_sgn sg (get_attributes gst) isg
216
217
218
219 {- no - valid result (Ok "" ) returned - only possibility of error - deal with this ? -}
220
221 show_obj sg ps lt attL ty sp win err
222 = x_form True (make_form ty sp win err) /./
223 exp
224 where
225 exp NONE = return ""
226
227 exp ( SOME [OutRadio obj_type, OutText obj_spec, OutRadio win] )
228 = display_fn (show_fn obj_spec) ./.
229 return ""
230 where
231 display_fn = case win of
232 "Own" -> own_win obj_type
233 "Scratch" -> scratch_win obj_type
234 _ -> own_win obj_type
235 show_fn = case obj_type of
236 "Trm" -> show_Trm sg ps lt attL
237 {-
238 "Thm" -> show_Thm sg ps lt attL
239 "Sgn" -> show_Sgn sg ps lt attL
240 "Dec" -> show_Dec sg ps lt attL
241 -}
242 _ -> show_error
243
244 -- exp _ = return ""
245
246 {-
247 handle
248 Syntax (e,inp) =>
249 let val err_mesg = unerr e
250 val where = under_line_input inp
251 val new_form = redo err_mesg where info
252 in show_obj xio sg ps lt attL new_form end
253 | Expect (t1,t2,inp) =>
254 let val err_mesg = eexperr t1 t2
255 val where = under_line_input inp
256 val new_form = redo err_mesg where info
257 in show_obj xio sg ps lt attL new_form end
258 | Fail s =>
259 let val err_mesg = "Error: "^ s
260 val where = ""
261 val new_form = redo err_mesg where info
262 in show_obj xio sg ps lt attL new_form end)
263 -}
264
265
266
267
268 {-
269 redo err whre (SOME [OutRadio obj_type, OutText obj_spec, OutRadio win])
270 = [
271 InComment "Parse Object",
272 InRadio "Type of Object" ["Trm","Thm","Sgn","Dec"],
273 InComment "Specification of Object",
274 InMultiText obj_spec,
275 InComment err,
276 InComment whre,
277 InRadio "Display Window" ["Own", "Scratch"]
278 ]
279 -}
280
281
282
283
284
285 show_Trm sg ps lt attL tm_rep
286 = unparse_Trm sg attL
287 (parse_tm (tgL,sg) tm_rep )
288 -- (parse_typed_Trm tm_rep ps sg)
289
290
291 {-
292 show_Thm sg ps lt attL th_rep
293 = unparse_Thm lt attL
294 (parse_Thm th_rep ps sg)
295
296
297
298 show_Sgn sg ps lt attL sg_rep
299 = unparse_Sgn lt attL
300 (parse_typed_Sgn sg_rep ps)
301
302
303
304 show_Dec sg ps lt attL dc_rep
305 = unparse_Dec lt attL
306 (parse_typed_Dec dc_rep ps sg)
307 -}
308
309
310 show_error s = "Bad Object"
311
312
313
314
315
316 own_win = x_display
317
318
319
320 scratch_win obj_type s = x_scratch ("\n\n" ++ obj_type ++ "\n\n" ++ s)
321
322
323
324 split_line = split '\n'
325
326
327
328
329 show_comment tr@(TreeSt t _ _)
330 = show_com t /./
331 (\ _ -> return tr )
332
333
334
335 edit_comment tr @ (TreeSt t tl gst)
336 = x_form True [InComment "Edit Comment", InMultiText "Comment:" com] /./
337 exp
338 where
339 exp (SOME [OutText com'])
340 = return ( TreeSt (set_comment com' t) tl gst )
341 exp _ = return tr
342
343 com = get_comment t
344
345
346
347 show_arguments tr@(TreeSt t _ _)
348 = show_args t ./.
349 return tr
350
351
352
353 show_args t@(Tree (Goal (SOME tac) op_args _ uid _ _ _ _) _ _ _ _)
354 = x_display title concat_args
355 where
356 concat_args = case op_args of
357 NONE -> "NONE"
358 SOME args -> foldr ((++).(\s->s++ "\n\n")) "" args
359 title = "Node: " ++ uid ++ "\nTactic: " ++ tac ++ "\nArguments:"
360
361 show_args t@(Tree (Goal _ _ _ _ _ _ _ _) _ _ _ _)
362 = x_set_status "No tactic applied!"
363
364
365 show_tactics t = x_show_tactics ./.
366 return t