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