What is a preterm parser?

Question

I am working with HOL-Light parser and keeping seeing references to preterm parser.

What is a preterm parser?

The most informative statement I find is from the HOL-Light reference for the parse_pretype function.

This is mostly an internal function; pretypes and preterms are used as an intermediate representation for typechecking and overload resolution and are not normally of concern to users.

Answer 1

Since HOL Light is based on $\lambda$ Calculus and HOL Light is typed and as we know there is untyped $\lambda$ Calculus and typed $\lambda$ Calculus, HOL Light starts by parsing something close to untyped $\lambda$ Calculus, creating pre-terms. Then it applies a typing checking and typing phase, along with resolving overloaded operators resulting is something closer to typed $\lambda$ Calculus. Obviously HOL is much more than typed $\lambda$ Calculus, but the point here is to understand what pre-term means with regards to parsing.

The only reference I have found for this is in

Lectures on the Curry-Howard Isomorphism
Section 1.2 Pre-terms and $\lambda$-terms.

Specifically how this is done in HOL Light is in the parser module:

The pre-terms are created with

let ptm = (parse_pteterm << lex << explode) input

and the type checking, etc. is done with

let term = (term_of_preterm << (retypecheck [])) ptm