Commits on Mar 1, 2024

1. Add a flag for printing types of subterms …

   This patch adds a new int ref flag `print_types_of_subterms`.
   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.
   
   This also changes the behavior of print_term to print the invented type variables inside a term as well.
   
   ```
     \# 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)`
   ```

   

   aqjune committed Mar 1, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for 13e4531
   • Browse repository at this point

   Copy the full SHA

   13e4531 View commit details

   Browse the repository at this point in the history