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