Unbreak these programs after Unicode IO support was added
[nofib.git] / real / veritas / Main.hs
1 module Main where
2
3 import Auto
4
5 import Tactics
6
7 import ThmTactics
8
9 import Display
10
11 import Tree
12
13 import Vtslib
14
15 import Editor
16
17 import Globals
18
19 import Getops
20
21 import Edlib
22
23 import Lookup
24
25 import X_interface
26
27 import Goals
28
29 import Type_defs
30
31 import Core_datatype
32
33 import Kernel
34
35 import Tags
36
37 import Parse
38
39 import System.IO
40
41
42 --proof_edit : string list * string list -> unit
43
44 main = do
45 hSetBinaryMode stdin True
46 hSetBinaryMode stdout True
47 ins <- getContents
48 putStr (main' ins)
49
50 main' instr
51 = rqts
52 where
53 ( _ , _ , rqts ) = edits
54 edits = proof_edit default_ds ( split '\n' args ) (instr , rsps , [1..])
55 default_ds = "" --home ++ "/VTS"
56 args = "" -- temp test
57 rsps = [0..] -- dummy response list
58
59
60
61
62
63
64
65
66
67
68
69 {-
70 -- = parse_spec_trm (strings_to_input [s])
71 -- (set_lookup_table initial_state lt) sg
72
73 -- other parsers later
74
75 parse_sgn lt sg s
76 = sgparse_spec_sgn (strings_to_input [s])
77 (set_lookup_table initial_state lt)
78
79 parse_dec lt sg s
80 = parse_spec_dec (strings_to_input [s])
81 (set_lookup_table initial_state lt) sg
82 -}
83
84
85
86 goto_next tr@(TreeSt t _ _)
87 = tree_top tr /./
88 (\ tr' -> case tree_search incomplete_tree False t of
89 ((iL,_):_) -> reTurn ( tree_goto iL tr )
90 _ -> case search_tree of
91 ((iL,_):_) -> reTurn(tree_goto iL tr')
92 _ -> reTurn tr
93 where
94 (TreeSt t' _ _) = tr'
95 search_tree = tree_search
96 incomplete_tree False t' )
97
98
99
100
101 incomplete_tree (Tree _ tl (SOME _) _ _ ) = False
102
103 incomplete_tree (Tree _ tl NONE _ _ ) = forall is_complete tl
104
105
106
107
108
109 goto_named tr@(TreeSt t _ _ )
110 = x_form True form /.>/
111 tree_top tr /./
112 exp
113 where
114 exp ( SOME [OutText uid] , tr' )
115 = case tree_search is_node True t' of
116 ((iL,_):_) -> reTurn ( tree_goto iL tr' )
117 _ -> x_set_status "No such node" ./.
118 reTurn tr
119 where
120 (TreeSt t' _ _ ) = tr'
121 is_node (Tree (Goal _ _ _ uid' _ _ _ _) _ _ _ _ )
122 = uid == uid'
123 exp _ = reTurn tr
124
125 form = [InComment "Goto Node",
126 InComment "",
127 InComment "Uid of Node",
128 InSingleText "" ""]
129
130 tree_cmdL =
131 [
132 ( "Top", tree_top ),
133 ( "P", tree_up ),
134 ( "PExpand", show_goal_cmd ),
135 ( "1Expand", show_subgoal_cmd 0),
136 ( "2Expand", show_subgoal_cmd 1),
137 ( "3Expand", show_subgoal_cmd 2),
138 ( "4Expand", show_subgoal_cmd 3),
139 ( "Theory", show_theory ),
140 ( "Object", show_object ),
141 ( "Comment", show_comment),
142 ( "Arguments", show_arguments),
143 ( "1", tree_down 0 ),
144 ( "2", tree_down 1),
145 ( "3", tree_down 2),
146 ( "4", tree_down 3),
147 ( "Next", goto_next),
148 ( "Named", goto_named),
149 ( "Undo",tree_undo),
150 ( "Tactic",show_tactics),
151 ( "Strip",strip_tac),
152 ( "Triv",triv_tac),
153 lift_tactic conj_tac,
154 lift_ordtactic gen_tac,
155 lift_tactic auto_tac,
156 lift_tactic reflex_tac,
157 lift_ordtactic disch_tac,
158 lift_tactic disj_tac,
159 lift_tactic eq_tac,
160 lift_tactic or_tac,
161 lift_tactic lemma_tac,
162 lift_tactic not_tac,
163 lift_tactic exists_elim_tac,
164 lift_tactic taut_tac,
165 lift_tactic axiom_tac,
166 lift_tactic hyp_tac,
167 -- lift_ordtactic split_tac,
168 lift_tactic induction_tac,
169 lift_tactic complete_tac
170 {-,
171 lift_tactic rewrite_tac,
172 -}
173 ]
174 strip_tac = strip (error "") auto_tac
175
176
177 triv_tac = triv auto_tac
178
179
180 edit = editor tree_cmdL initialize update_state my_quit finish
181
182
183 proof_edit default_ds argL
184 -- = getops "d:s:t:" argL
185 = exp ( [] , [] ) --('t',SOME "Trm")], ["hello"]) --temp arg parse
186 where
187 exp _ --(options, [arg])
188 = edit
189 `handle`
190 err_handler
191 err_handler mesg = x_error mesg /./
192 ( \ _ -> proof_edit default_ds argL )