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 )