1 module Goals where 2 3 import Unparse 4 5 import X_interface 6 7 import Edlib 8 9 import Core_datatype 10 11 import Vtslib 12 13 import Tree 14 15 import Globals 16 17 import Lookup -- stub 18 19 import Parse 20 21 import Kernel 22 23 import Sub_Core1 24 25 import Sub_Core2 26 27 import Sub_Core3 28 29 import Sub_Core4 30 31 import Type_defs 32 33 import Tags 34 35 {- 36 (******************************************************************************) 37 (* A goal consists of: a tactic name, a list of arguments, a comment, a *) 38 (* unique identifier and a specification. *) 39 (******************************************************************************) 40 -} 41 42 data GOAL = Goal ( Option String ) 43 ( Option [String] ) -- arguments if any 44 ( Option String ) -- comment if any 45 String -- unique identifier 46 Obj -- spec (goal) 47 Bool -- read only? 48 Sgn -- its signature 49 Lookup_table -- its lookup table 50 51 52 53 54 data Obj = TrmSpec ITrm | 55 ThmSpec ITrm | 56 SgnSpec ISgn | 57 DecSpec IDec 58 59 60 61 62 data Done = TrmDone Trm | 63 ThmDone Thm | 64 SgnDone Sgn | 65 DecDone Dec 66 67 68 69 70 71 show_option :: (String -> a) -> (b -> String) -> (Option b) -> a 72 73 show_option xfn gfn NONE = xfn "None" 74 75 show_option xfn gfn (SOME x) = xfn (gfn x) 76 77 78 79 summary_depth :: Int 80 81 summary_depth = 4 82 83 84 85 is_done :: (Option a) -> String 86 87 is_done NONE = "" 88 89 is_done (SOME _) = "Done" 90 91 92 93 94 short :: Int -> String -> String 95 96 short = short' -- Check that they are the same 97 98 99 100 short' :: Int -> String -> String 101 102 short' _ [] = [] 103 104 short' 0 _ = "..." 105 106 short' i ('\n' : l) = ' ' : remove_spaces (i-1) l 107 108 short' i (c : l) = c : short' (i-1) l 109 110 111 112 113 114 remove_spaces :: Int -> String -> String 115 116 remove_spaces i ( ' ' : l) = remove_spaces i l 117 118 remove_spaces i ( '\n' : l) = remove_spaces i l 119 120 remove_spaces i l = short' i l 121 122 123 124 125 126 depth_print_tm i l sg tm = short 50 (unparse_trm sg l tm) 127 128 depth_print_sg i l sg isg = short 50 (unparse_sgn sg l isg) 129 130 depth_print_dc i l sg dc = short 50 (unparse_dec sg l dc) 131 132 133 134 135 {- 136 show_parent gst [] 137 = x_unset_parent 138 139 show_parent gst ((_,t):_) 140 = x_set_parent done summary 141 where 142 (done,summary) = show_summary (get_attributes gst) t 143 -} 144 145 146 147 show_summary attL (Tree (Goal _ _ _ _ (TrmSpec tm) _ sg _) _ dn _ _) 148 = (is_done dn, depth_print_tm summary_depth attL sg tm) 149 150 show_summary attL (Tree (Goal _ _ _ _ (ThmSpec tm) _ sg _) _ dn _ _) 151 = (is_done dn, depth_print_tm summary_depth attL sg tm) 152 153 show_summary attL (Tree (Goal _ _ _ _ (SgnSpec isg) _ sg _) _ dn _ _) 154 = (is_done dn, depth_print_sg summary_depth attL sg isg) 155 156 show_summary attL (Tree (Goal _ _ _ _ (DecSpec dc) _ sg _) _ dn _ _) 157 = (is_done dn, depth_print_dc summary_depth attL sg dc) 158 159 160 161 162 163 164 show_goal :: Global_state -> (TREE GOAL b c) -> Xio_fn 165 166 show_goal gst t@(Tree (Goal tac args com uid obj rw _ lt) _ _ _ _) 167 = show_node uid obj ... 168 show_option x_set_tactic id tac ... 169 show_option x_set_argument head args ... 170 show_option x_set_comment (short 50) com ... 171 x_set_rw (if rw then "Editable" else "Read Only") ... 172 x_set_goal done summary 173 where 174 (done,summary) = show_summary (get_attributes gst) t 175 -- (done,summary) = show_summary [] t 176 177 178 179 180 show_node uid (TrmSpec tm) 181 = x_set_node ("Trm Node: " ++ uid) 182 183 show_node uid (ThmSpec tm) 184 = x_set_node ("Thm Node: " ++ uid) 185 186 show_node uid (DecSpec dc) 187 = x_set_node ("Dec Node: " ++ uid) 188 189 show_node uid (SgnSpec sg) 190 = x_set_node ("Sgn Node: " ++ uid) 191 192 193 194 195 196 show_subgoals gst goalL 197 = x_set_subgoals (map (show_summary (get_attributes gst)) goalL) 198 199 200 201 show_done NONE = x_set_done "Incomplete" 202 203 show_done (SOME _) = x_set_done "Complete" 204 205 206 207 208 209 {- old initialize 210 initialize (TreeSt t@(Tree goal goalL dn _ _ ) spine gst ) 211 = show_parent gst spine ... 212 show_done dn ... 213 show_goal gst t ... 214 show_subgoals gst goalL 215 -} 216 217 initialize dset thy styp spec NONE 218 = get_tree dset thy styp spec NONE /./ 219 exp 220 where 221 exp ( SOME (tr@(TreeSt t@(Tree goal goalL dn _ _) spine gst))) 222 = show_goal gst t ... 223 show_subgoals gst goalL ./. 224 reTurn tr 225 exp NONE 226 = end_x ./. 227 return_err "no state" 228 229 230 get_tree :: (Option String) -> (Option String) -> (Option String) -> 231 (Option String) -> (Option String) -> Xin -> 232 Xst ( MayBe (Option (Tree_state GOAL b Global_state )) String ) 233 234 get_tree dset thy styp spec errmesg 235 = x_form True (input_form dset thy styp spec errmesg) /./ 236 exp 237 where 238 exp NONE = reTurn NONE 239 240 exp ( SOME [OutText ds, OutText ty, OutText sp, OutRadio st] ) 241 = parse_fn /.>/ 242 genuid /./ 243 exp2 244 where 245 parse_fn = case st of 246 "Thm" -> mkspec ThmSpec parse_trm sp 247 "Trm" -> mkspec TrmSpec parse_trm sp 248 -- "Dec" -> mkspec DecSpec parse_dec sp 249 -- "Sgn" -> mkspec SgnSpec parse_sgn sp 250 -- _ -> return_err "Bad Type" 251 mkspec ctr p_fn sp 252 = case p_fn sg ps sp of 253 Ok res -> reTurn ( ctr res ) 254 Bad mesg -> return_err mesg 255 where 256 ps = default_tag_tbl 257 258 exp2 ( obj , uid ) 259 = reTurn ( SOME tst ) 260 where 261 tst = TreeSt tr [] gst 262 tr = Tree gl [] NONE ( \ x y -> y ) NONE 263 gl = Goal NONE NONE NONE uid obj True sg lt 264 lt = [] --create_lookup_table isg 265 at = [] --defaults 266 gst = ( 0 , [] , default_tag_tbl ) 267 268 exp _ = error "unimplemented in get_tree" 269 sg = empty --erestore_Sgn (ds,ty) 270 isg = internal_Sgn sg 271 272 {- 273 handle 274 Syntax (e,inp) => 275 let val err = unerr e 276 val where = under_line_input inp 277 in get_tree (SOME ds) (SOME ty) (SOME st) (SOME sp) 278 (SOME (err ^ "\n" ^ where)) xio 279 end 280 | Expect (t1,t2,inp) => 281 let val err = eexperr t1 t2 282 val where = under_line_input inp 283 in get_tree (SOME ds) (SOME ty) (SOME st) (SOME sp) 284 (SOME (err ^ "\n" ^ where)) xio 285 end 286 | Fail s => 287 let val err = "Error: "^ s 288 in get_tree (SOME ds) (SOME ty) (SOME st) (SOME sp) 289 (SOME err) xio 290 end 291 | _ => 292 293 let val err = "Error in specification" 294 in get_tree (SOME ds) (SOME ty) (SOME st) (SOME sp) 295 (SOME err) xio 296 end 297 ) 298 -} 299 300 301 input_form dset thy styp spec errmesg 302 = [ InComment "XVTSEDIT VERSION 1.1", 303 InSingleText "Dataset" ( case dset of 304 SOME ds -> ds 305 _ -> default_ds ), 306 InSingleText "Theory " ( case thy of 307 SOME ty -> ty 308 _ -> default_ty ), 309 InMultiText "Spec " ( case spec of 310 SOME sp -> sp 311 _ -> "" ), 312 InRadio "Type " 313 ( case styp of 314 SOME st -> my_index st types 315 _ -> 0 ) 316 types ] ++ 317 (case errmesg of 318 SOME err -> [ InComment err ] 319 NONE -> [] ) 320 321 322 types = ["Thm","Trm","Sgn","Dec"] 323 324 325 326 my_index :: Eq b => b -> [b] -> Int 327 328 my_index s (s' : l) = if s == s' then 0 else 1 + my_index s l 329 330 my_index s [] = 0 331 332 333 default_ty = "empty" 334 335 default_ds = "default_ds not passed in yet" 336 337 338 339 340 341 342 {- 343 (******************************************************************************) 344 (* When sorted out equalities, should check differences and only update *) 345 (* those fields which differ *) 346 (******************************************************************************) 347 -} 348 349 update_state (TreeSt ( Tree goal1 goalL1 dn1 _ _ ) spine1 gst1 ) 350 (TreeSt t@( Tree goal2 goalL2 dn2 _ _ ) spine2 gst2 ) 351 = ((show_goal gst2 t) ... 352 (show_subgoals gst2 goalL2)) 353 354 355 356 my_quit current 357 = x_form True form /./ exp 358 where 359 exp NONE = reTurn False 360 exp ( SOME _ ) = reTurn True 361 form = [InComment "\n\nSelect ok to Quit\n\n"] 362 363 364 365 finish = end_x ./. reTurn (error "Finish state evaluated") 366