Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add a new flag print_types_of_subterms #92

Merged
merged 1 commit into from
Mar 1, 2024
Merged

Conversation

aqjune
Copy link
Contributor

@aqjune aqjune commented Feb 26, 2024

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 aqjune changed the title Add a flag for printing invented type vars in a term Add a new flag print_types_of_subterms Feb 27, 2024
@aqjune
Copy link
Contributor Author

aqjune commented Feb 27, 2024

Addressed comments. :)

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)`
```
@jrh13 jrh13 merged commit c518278 into jrh13:master Mar 1, 2024
2 checks passed
@aqjune aqjune deleted the typevar-print branch March 1, 2024 21:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants