Merge pull request #92 from aqjune/typevar-print

Add a new flag `print_types_of_subterms`

Help/print_types_of_subterms.hlp

@@ -0,0 +1,56 @@
+\DOC print_types_of_subterms
+
+\TYPE {print_types_of_subterms : int ref}
+
+\SYNOPSIS
+Flag controlling the level of printing types of subterms.
+
+\DESCRIBE
+The reference variable {print_types_of_subterms} is one of several
+settable parameters controlling printing of terms by {pp_print_term}, and hence
+the automatic printing of terms and theorems at the toplevel.
+
+When it is {0}, {pp_print_term} does not print the types of subterms.
+When it is {1}, as it is by default, {pp_print_term} only prints types of subterms containing invented type variables.
+When it is {2}, {pp_print_term} prints the types of all constants and variables in the term.
+
+\FAILURE
+Not applicable.
+
+\EXAMPLE
+{
+  # loadt "Library/words.ml";;
+  ...
+
+  # `word_join (word 10:int64) (word 20:int64)`;;
+  Warning: inventing type variables
+  val it : term =
+    `(word_join:(64)word->(64)word->(?194629)word) (word 10) (word 20)`
+  # `word_join (word 10:int64) (word 20:int64):int128`;;
+  val it : term = `word_join (word 10) (word 20)`
+
+  # print_types_of_subterms := 0;;
+  val it : unit = ()
+  # `word_join (word 10:int64) (word 20:int64)`;;
+  Warning: inventing type variables
+  val it : term = `word_join (word 10) (word 20)`
+  # `word_join (word 10:int64) (word 20:int64):int128`;;
+  val it : term = `word_join (word 10) (word 20)`
+
+  # print_types_of_subterms := 2;;
+  val it : unit = ()
+  # `word_join (word 10:int64) (word 20:int64)`;;
+  Warning: inventing type variables
+  val it : term =
+    `(word_join:(64)word->(64)word->(?194609)word) ((word:num->(64)word) 10)
+    ((word:num->(64)word) 20)`
+  # `word_join (word 10:int64) (word 20:int64):int128`;;
+  val it : term =
+    `(word_join:(64)word->(64)word->(128)word) ((word:num->(64)word) 10)
+    ((word:num->(64)word) 20)`
+}
+
+\SEEALSO
+pp_print_term, type_invention_error, type_invention_warning
+
+\ENDDOC

Help/type_invention_error.hlp

@@ -42,6 +42,6 @@ type variables yourself:
 }
 
 \SEEALSO
-retypecheck, term_of_preterm, type_invention_warning.
+print_types_of_subterms, retypecheck, term_of_preterm, type_invention_warning.
 
 \ENDDOC

Help/type_invention_warning.hlp

@@ -51,6 +51,6 @@ you are rewriting with ad-hoc set theory lemmas generated like this:
 }
 
 \SEEALSO
-retypecheck, term_of_preterm, type_invention_error.
+print_types_of_subterms, retypecheck, term_of_preterm, type_invention_error.
 
 \ENDDOC

printer.ml

@@ -144,6 +144,15 @@ let typify_universal_set = ref true;;
 
 let print_all_thm = ref true;;
 
+(* ------------------------------------------------------------------------- *)
+(* Flag controlling whether types of subterms must be printed.               *)
+(* 0: Do not print the types of subterms                                     *)
+(* 1 (defualt) : Only print types containing invented type variables         *)
+(* 2: Print the types of constants and variables                             *)
+(* ------------------------------------------------------------------------- *)
+
+let print_types_of_subterms = ref 1;;
+
 (* ------------------------------------------------------------------------- *)
 (* Get the name of a constant or variable.                                   *)
 (* ------------------------------------------------------------------------- *)
@@ -422,7 +431,21 @@ let pp_print_term =
       else if (is_const hop || is_var hop) && args = [] then
         let s' = if parses_as_binder s || can get_infix_status s || is_prefix s
                  then "("^s^")" else s in
-        pp_print_string fmt s'
+        let rec has_invented_typevar (ty:hol_type): bool =
+          if is_vartype ty then (dest_vartype ty).[0] = '?'
+          else List.exists has_invented_typevar (snd (dest_type ty)) in
+        if !print_types_of_subterms = 2 ||
+           (!print_types_of_subterms = 1 && has_invented_typevar (type_of hop))
+        then
+          (pp_open_box fmt 0;
+          pp_print_string fmt "(";
+          pp_print_string fmt s';
+          pp_print_string fmt ":";
+          pp_print_type fmt (type_of hop);
+          pp_print_string fmt ")";
+          pp_close_box fmt ())
+        else
+          pp_print_string fmt s'
       else
         let l,r = dest_comb tm in
         (pp_open_hvbox fmt 0;