History log of /seL4-l4v-master/HOL4/src/parse/qbuf.sig
Revision Date Author Comments
# 036d54c1 05-Jul-2019 Michael Norrish <Michael.Norrish@nicta.com.au>

Add a push entry-point to the qbuf type (used in parsing)


# 3f252166 13-Mar-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Work towards use of PolyML.pretty type for most pretty-printing

Compiles up to src/parse under Poly/ML


# 32bf1e49 02-Feb-2015 Piotr Trojanek <piotr.trojanek@gmail.com>

extra semicolons removed from (some) .sig files


# b4161465 30-Mar-2014 Michael Norrish <Michael.Norrish@nicta.com.au>

Implement most of a new Datatype function with nicer syntax.

(Pair-programming with Magnus who wanted it.) Still need to
implement change to EmitTeX.


# 512123cb 22-Apr-2005 Konrad Slind <konrad.slind@gmail.com>

Adapting to new Basis (and SML/NJ).


# 275a997c 03-Sep-2002 Keith Wansbrough <keith@lochan.org>

This commit contains the initial version of the error-location
reporting code I have been working on over the last couple of weeks.

Basically, error messages will now report the source location they
relate to, enabling users to locate bugs more easily within large
definitions.

So far, errors are reported by the lexer, the term parser, and the
datatype parser. Type parser errors will follow, and (hopefully)
typecheck errors.

src/0/locn is a small location-handling library. locn.locn is the
type of locations, and 'a locn.located is a synonym for 'a *
locn.locn. There is a location, Loc_None, for compiler-generated
text, and another, Loc_Unknown, for text of unknown location.

src/0/Feedback now includes some functions for generating located errors.

The lexer now returns located tokens, term_token and type_token
maintain the locations, and parse_term maintains them *internally* on
each terminal and nonterminal. When the system is complete, locations
will persist into absyn and preterm (if I understand the code
correctly!) to enable the typechecker to yield located errors.

I would appreciate any feedback:

* Is the performance impact significant?
* Are any error messages incorrect? (there's a lot of
location-manipulation code in parse_term, some of which I don't
fully understand, and surely some bugs)
* Have I broken anything for anyone, or am I likely to?

The actual output format of the location information is provisional
only, and I intend to generate absolute file positions (rather than
fragment offsets) shortly.

--KW 8-)

NB: tags pre-locn-change and post-locn-change cover this commit.


# a1dfcb9b 26-Jul-2002 Michael Norrish <Michael.Norrish@nicta.com.au>

A complete re-implementation of lexing. Speeds things up considerably
through the use of mosmllex. (The example at the bottom of term_tokens.sml
goes through four to five times faster than it used to.) The basic
design is now more stateful than it used to be. There is a new type,
called the qbuf, which provides buffered access to a quotation. The
implementation of parse_type changes completely because it can no longer
do the monadic-parsing trick of backing up over failed parses. The
implementation of the term parser doesn't really change at all.