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.
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
