fol/README

This is a sample parser for first-order logic.   The grammar
was contributed by Frank Pfenning.

The parser is defined by the files

  fol.lex       (* defines lexer *)
  fol.grm       (* defines grammar *)
  link.sml	(* constructs basic parser structures *)
  absyn.sml	(* a trivial abstract syntax *)
  interface.sml (* interface to lexer and parser properties *)
  parse.sml	(* driver functions *)
  sources.cm    (* cm description file *)

To compile this example, type

	- CM.make "sources.cm";

in this directory.  CM will invoke ml-lex and ml-yacc to process the
lexer specification calc.lex and the grammar specification calc.grm
respectively.  Then it will compile the resulting SML source files

  fol.lex.sml
  fol.grm.sig
  fol.grm.sml

and the other sml source files.

The end result of loading these files is a structure Parse containing
the following top-level driver functions:

  val prog_parse : string -> Absyn.absyn 
   (* parse a program from a string *)

  val query_parse : string -> Absyn.absyn
   (* parse a query from a string *)

  val file_parse : string -> Absyn.absyn
   (* parse a program in a file *)

  val top_parse : unit -> Absyn.absyn
   (* parse a query from the standard input *)


The file list.fol is a sample input file that can be parsed using
the file_parse function:

  - Parse.file_parse "list.fol";


NOTE: The CM description file sources.cm mentions the ml-yacc library
(ml-yacc-lib.cm). CM's search path should be configured so that this
library will be found.  This should normally be the case if SML/NJ is
properly installed.
