1(*===================================================================== *) 2(* FILE : holmode.sml *) 3(* DESCRIPTION : some ml-callbacks used by hol-mode *) 4(* ===================================================================== *) 5 6 7 8(* 9 val use_goal_stack = true; 10 val context_string_opt = SOME ("f (SOME x) (SOME 0) = T"); 11 val term_string = "f"; 12 13 (set_goal ([], ``f y = F``)) 14*) 15 16val _ = load "Sanity"; 17 18local 19 fun repeat_print s n = if (n <= 0) then () else (print s; repeat_print s (n-1)); 20 val print_space = repeat_print " "; 21 fun print_width n s = (print s; (print_space (n - (size s)))); 22 fun print_header c s = 23 (print s;print "\n";repeat_print c (if (size s) < 70 then size s else 70);print "\n"); 24 25in 26 27fun type_of_in_context use_goal_stack context_string_opt term_string = 28let 29 fun term_does_type_match t1 t2 = 30 let 31 val (vsubst, _) = match_term t1 t2 32 in 33 null vsubst 34 end handle HOL_ERR _ => false 35 36 37 (*no context*) 38 val term_no_context_term = 39 Parse.parse_in_context [] [QUOTE term_string] 40 41 (*user context*) 42 val context_term_opt = 43 if isSome context_string_opt then 44 total (Parse.parse_in_context []) [QUOTE (valOf context_string_opt)] 45 else NONE; 46 47 val (term_user_context_term,context_matchesL) = 48 if not (isSome context_term_opt) then 49 (term_no_context_term, []) 50 else ( 51 Parse.parse_in_context (free_vars (valOf context_term_opt)) [QUOTE term_string], 52 53 HOLset.listItems (HOLset.addList (empty_tmset, 54 (find_terms (term_does_type_match (term_no_context_term)) 55 (valOf context_term_opt))))); 56 57 58 (*goalstack context*) 59 val goalstack_context = (if use_goal_stack then 60 (flatten (map (fn (ts,t) => t::ts) (proofManagerLib.top_goals()))) 61 else []) handle Interrupt => raise Interrupt | _ => []; 62 63 val term_goalstack_context_term = 64 Parse.parse_in_context (free_varsl goalstack_context) [QUOTE term_string] 65 66 val goalstack_matchesL = HOLset.listItems ( 67 HOLset.addList (empty_tmset, 68 flatten (map (find_terms (term_does_type_match (term_no_context_term))) 69 goalstack_context))) 70in 71 (term_no_context_term, term_user_context_term, term_goalstack_context_term, 72 context_matchesL, goalstack_matchesL) 73end; 74 75 76 77fun print_type_of_in_context use_goal_stack context_string_opt term_string = 78let 79 val (t1, t2, t3, tL1, tL2) = 80 type_of_in_context use_goal_stack context_string_opt term_string; 81 82 val t1s = term_to_string t1 83 val t2s = term_to_string t2 84 val t3s = term_to_string t3 85 val tL1s = map term_to_string tL1 86 val tL2s = map term_to_string tL2 87 88 val list_max = foldl (fn (a,b) => if a > b then a else b) 0 89 90 fun print_term_width w (t,s) = 91 (print_width w s; 92 print " "; 93 print (type_to_string (type_of t));print "\n") 94 val print_term = print_term_width 0; 95 96 97 fun print_term_list l = 98 let 99 val max_width = list_max (map (size o snd) l) 100 in 101 map (print_term_width max_width) l;() 102 end; 103 104in 105 print "\n\n\n\n"; 106 print_header "=" ("\nType information for \"" ^ term_string ^ "\""); 107 print "\n\n"; 108 print_header "-" "No context:"; 109 print_term (t1, t1s); 110 (if ((aconv t1 t2) orelse not (isSome context_string_opt)) then () else ( 111 print "\n\n"; 112 print_header "-" ("In context \"" ^ (valOf context_string_opt) ^ "\":"); 113 print_term (t2,t2s))); 114 (if (aconv t1 t3) then () else ( 115 print "\n\n"; 116 print_header "-" ("In goalstack context:"); 117 print_term (t3, t3s))); 118 (if (null tL1) then () else ( 119 print "\n\n"; 120 print_header "-" ("Matching subterms in context \"" ^ (valOf context_string_opt) ^ "\":"); 121 print_term_list (zip tL1 tL1s))); 122 (if (null tL2) then () else ( 123 print "\n\n"; 124 print_header "-" ("Matching subterms in goalstack-context:"); 125 print_term_list (zip tL2 tL2s))); 126 print "\n\n\n\n" 127end; 128 129 130fun print_current_load_paths () = 131let 132 val paths = !loadPath 133 val _ = print "\n\n"; 134 val _ = print_header "-" "Current loadPath"; 135 val _ = map (fn t => (print " ";print t; print "\n")) paths 136 val _ = print "\n"; 137in 138 () 139end; 140 141 142fun emacs_hol_mode_loaded () = 143 ["HOL_Interactive", "Meta", 144 "Array", "ArraySlice", "BinIO", "BinPrimIO", "Bool", "Byte", 145 "CharArray", "CharArraySlice", "Char", "CharVector", 146 "CharVectorSlice", "CommandLine.name", "Date", "General", "IEEEReal", 147 "Int", "IO", "LargeInt", "LargeReal", "LargeWord", "List", "ListPair", 148 "Math", "Option", "OS", "Position", "Real", "StringCvt", "String", 149 "Substring", "TextIO", "TextPrimIO", "Text", "Timer", "Time", 150 "VectorSlice", "Vector", "Word8Array", "Word8ArraySlice", 151 "Word8Vector", "Word8VectorSlice", "Word8", "Word"] @ (Meta.loaded()); 152 153fun print_hol_mode_loaded () = 154let 155 val loaded = emacs_hol_mode_loaded(); 156 val sorted_loaded = sort (fn s1 => fn s2 => String.< (s1, s2)) loaded 157 val _ = print "\n\n"; 158 val _ = print_header "-" "Loaded Modules"; 159 val _ = List.map (fn t => (print " ";print t; print "\n")) sorted_loaded 160 val _ = print "\n"; 161in 162 () 163end; 164 165fun print_current_hol_status hol_ex holmake_ex () = let 166 val _ = HOL_Interactive.print_banner() 167 val _ = print "\n"; 168 val _ = (print "Hol executable : "; print hol_ex; print "\n"); 169 val _ = (print "Holmake executable: "; print holmake_ex; print "\n"); 170 val _ = (print "Holdir : "; print HOLDIR; print "\n"); 171 val _ = print_current_load_paths(); 172 val _ = print_hol_mode_loaded(); 173in 174 () 175end; 176 177end; 178