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 )