File: READ-ME

package info (click to toggle)
hol88 2.02.19940316dfsg-5
  • links: PTS
  • area: main
  • in suites: bookworm
  • size: 65,816 kB
  • sloc: ml: 199,939; ansic: 9,666; sh: 6,913; makefile: 6,032; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (15 lines) | stat: -rw-r--r-- 669 bytes parent folder | download | duplicates (11) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
 
This directory contains a grammar describing a parser for the
programming language of the library "prog_logic88".  

The file tiny.grm contains the grammar for the parser.  tiny_help.ml
holds the definitions of the action symbols.  Heavy use of 
antiquotation is made.

The file examples.ml is a rewrite of the examples file from the
programming logics library.  It makes use of the newly constructed
parser rather than the lisp hacks previously used.

To remake the parser, edit the Makefile to reflect the appropriate
pathnames.  To remake from scratch, run the generator over the file
tiny.grm.  To load into HOL, edit the file loader.ml, and perform
a loadf on it.