Commit 63bdcb85 authored by POTTIER Francois's avatar POTTIER Francois

Distinguished the demos calc-incremental and calc-inspection.

parent 1152829c
DEMOS := calc calc-two calc-param calc-incremental
DEMOS := calc calc-two calc-param calc-incremental calc-inspection
.PHONY: all clean
......
......@@ -9,7 +9,7 @@ endif
# We assume that menhirLib has been installed in such a
# way that ocamlfind knows about it.
MENHIRFLAGS := --table --inspection
MENHIRFLAGS := --table
# -- infer is automatically added by ocamlbuild.
OCAMLBUILD := ocamlbuild -use-ocamlfind -use-menhir -menhir "$(MENHIR) $(MENHIRFLAGS)" -package menhirLib
......
(* Introduce a short name for the incremental parser API. *)
(* A short name for the incremental parser API. *)
module I =
Parser.MenhirInterpreter
(* A custom symbol printer. *)
(* The loop which drives the parser. At each iteration, we analyze a
result produced by the parser, and act in an appropriate manner. *)
let print_symbol symbol =
let open I in
match symbol with
| X (T T_TIMES) ->
"*"
| X (T T_RPAREN) ->
")"
| X (T T_PLUS) ->
"+"
| X (T T_MINUS) ->
"-"
| X (T T_LPAREN) ->
"("
| X (T T_INT) ->
"INT"
| X (N N_expr) ->
"expr"
| X (N N_main) ->
"main"
| X (T T_EOL) ->
"EOL"
| X (T T_DIV) ->
"/"
| X (T T_error) ->
"error"
(* [lexbuf] is the lexing buffer. [result] is the last result produced
by the parser. *)
module P =
Printers.Make(I) (struct
let arrow = " -> "
let dot = "."
let space = " "
let print_symbol = print_symbol
end)
(* A custom element printer. *)
let print_element e : string =
match e with
| I.Element (s, v, _, _) ->
let open I in
match incoming_symbol s with
| T T_TIMES ->
"*"
| T T_RPAREN ->
")"
| T T_PLUS ->
"+"
| T T_MINUS ->
"-"
| T T_LPAREN ->
"("
| T T_INT ->
string_of_int v
| N N_expr ->
string_of_int v
| N N_main ->
string_of_int v
| T T_EOL ->
""
| T T_DIV ->
"/"
| T T_error ->
"error"
(* Debugging. *)
let dump env =
Printf.fprintf stderr "Stack height: %d\n%!" (I.length (I.view env));
Printf.fprintf stderr "Stack view:\n%s\n%!" (P.print_env print_element env);
begin match Lazy.force (I.view env) with
| I.Nil ->
()
| I.Cons (I.Element (current, _, _, _), _) ->
Printf.fprintf stderr "Current state: %d\n%!" (Obj.magic current);
let items = I.items current in
Printf.fprintf stderr "#Items: %d\n%!" (List.length items);
List.iter (fun item ->
Printf.fprintf stderr "%s\n%!" (P.print_item item)
) items
end;
print_newline()
(* Define the loop which drives the parser. At each iteration,
we analyze a result produced by the parser, and act in an
appropriate manner. *)
let rec loop linebuf (result : int I.result) =
let rec loop lexbuf (result : int I.result) =
match result with
| I.InputNeeded env ->
dump env;
(* The parser needs a token. Request one from the lexer,
and offer it to the parser, which will produce a new
result. Then, repeat. *)
let token = Lexer.token linebuf in
let startp = linebuf.Lexing.lex_start_p
and endp = linebuf.Lexing.lex_curr_p in
let token = Lexer.token lexbuf in
let startp = lexbuf.Lexing.lex_start_p
and endp = lexbuf.Lexing.lex_curr_p in
let result = I.offer result (token, startp, endp) in
loop linebuf result
loop lexbuf result
| I.AboutToReduce (env, prod) ->
dump env;
let result = I.resume result in
loop linebuf result
loop lexbuf result
| I.HandlingError env ->
(* The parser has suspended itself because of a syntax error. Stop. *)
Printf.fprintf stderr
"At offset %d: syntax error.\n%!"
(Lexing.lexeme_start linebuf)
(Lexing.lexeme_start lexbuf)
| I.Accepted v ->
(* The parser has succeeded and produced a semantic value. Print it. *)
Printf.printf "%d\n%!" v
......@@ -123,9 +39,9 @@ let rec loop linebuf (result : int I.result) =
(* Initialize the lexer, and catch any exception raised by the lexer. *)
let process (line : string) =
let linebuf = Lexing.from_string line in
let lexbuf = Lexing.from_string line in
try
loop linebuf (Parser.Incremental.main())
loop lexbuf (Parser.Incremental.main())
with
| Lexer.Error msg ->
Printf.fprintf stderr "%s%!" msg
......
.PHONY: all clean test
# Find Menhir.
ifndef MENHIR
MENHIR := $(shell ../find-menhir.sh)
endif
# We use the table back-end, and link against menhirLib.
# We assume that menhirLib has been installed in such a
# way that ocamlfind knows about it.
MENHIRFLAGS := --table --inspection
# -- infer is automatically added by ocamlbuild.
OCAMLBUILD := ocamlbuild -use-ocamlfind -use-menhir -menhir "$(MENHIR) $(MENHIRFLAGS)" -package menhirLib
MAIN := calc
all:
$(OCAMLBUILD) $(MAIN).native
clean:
rm -f *~
$(OCAMLBUILD) -clean
test: all
@echo "The following command should print 42:"
echo "(1 + 2 * 10) * 2" | ./$(MAIN).native
module Make
(I : MenhirLib.IncrementalEngine.EVERYTHING)
(User : sig
val arrow: string (* should include space on both sides *)
val dot: string
val space: string
val print_symbol: I.xsymbol -> string
end)
= struct
open User
(* Buffer and string utilities. *)
let out =
Buffer.add_string
let with_buffer f x =
let b = Buffer.create 128 in
f b x;
Buffer.contents b
let into_buffer f b x =
out b (f x)
(* Printing a list of symbols. An optional dot is printed at offset
[i] into the list [symbols], if this offset lies between [0] and
the length of the list (included). *)
let rec buffer_symbols b i symbols =
if i = 0 then begin
out b dot;
out b space;
buffer_symbols b (-1) symbols
end
else begin
match symbols with
| [] ->
()
| symbol :: symbols ->
out b (print_symbol symbol);
out b space;
buffer_symbols b (i - 1) symbols
end
(* Printing an item. *)
let buffer_item b (prod, i) =
out b (print_symbol (I.lhs prod));
out b arrow;
buffer_symbols b i (I.rhs prod)
(* Printing a production (without a dot). *)
let buffer_production b prod =
buffer_item b (prod, -1)
let print_item =
with_buffer buffer_item
let print_production =
with_buffer buffer_production
(* Printing an element as a symbol. *)
let print_element_as_symbol element =
match element with
| I.Element (s, _, _, _) ->
print_symbol (I.X (I.incoming_symbol s))
let buffer_element_as_symbol =
into_buffer print_element_as_symbol
(* Printing a stack or an environment. These functions are parameterized
over an element printer. [print_element_as_symbol] can be used for
this purpose; but the user can define other printers if desired. *)
let buffer_stack buffer_element b stack =
I.foldr (fun element () ->
buffer_element b element;
out b space
) stack ()
let buffer_env buffer_element b env =
buffer_stack buffer_element b (I.view env)
let print_stack print_element stack =
with_buffer (buffer_stack (into_buffer print_element)) stack
let print_env print_element env =
with_buffer (buffer_env (into_buffer print_element)) env
end
module Make
(I : MenhirLib.IncrementalEngine.EVERYTHING)
(User : sig
val arrow: string (* should include space on both sides *)
val dot: string
val space: string
val print_symbol: I.xsymbol -> string
end)
: sig
(* Printing an element as a symbol. This prints just the symbol
that this element represents; nothing more. *)
val buffer_element_as_symbol: Buffer.t -> I.element -> unit
val print_element_as_symbol: I.element -> string
(* Printing a stack or an environment. These functions are parameterized
over an element printer. [print_element_as_symbol] can be used for
this purpose; but the user can define other printers if desired. *)
val buffer_stack: (Buffer.t -> I.element -> unit) -> Buffer.t -> I.element I.stream -> unit
val print_stack: (I.element -> string) -> I.element I.stream -> string
val buffer_env: (Buffer.t -> I.element -> unit) -> Buffer.t -> I.env -> unit
val print_env: (I.element -> string) -> I.env -> string
(* Printing an item. *)
val buffer_item: Buffer.t -> I.item -> unit
val print_item: I.item -> string
(* Printing a production. *)
val buffer_production: Buffer.t -> I.production -> unit
val print_production: I.production -> string
end
This variant of the calc demo uses Menhir with the --table and --inspection
options. It illustrates how to inspect the intermediate states produced by
the parser.
(* A short name for the incremental parser API. *)
module I =
Parser.MenhirInterpreter
(* A custom symbol printer. *)
let print_symbol symbol =
let open I in
match symbol with
| X (T T_TIMES) ->
"*"
| X (T T_RPAREN) ->
")"
| X (T T_PLUS) ->
"+"
| X (T T_MINUS) ->
"-"
| X (T T_LPAREN) ->
"("
| X (T T_INT) ->
"INT"
| X (N N_expr) ->
"expr"
| X (N N_main) ->
"main"
| X (T T_EOL) ->
"EOL"
| X (T T_DIV) ->
"/"
| X (T T_error) ->
"error"
module P =
Printers.Make(I) (struct
let arrow = " -> "
let dot = "."
let space = " "
let print_symbol = print_symbol
end)
(* A custom element printer. *)
let print_element e : string =
match e with
| I.Element (s, v, _, _) ->
let open I in
match incoming_symbol s with
| T T_TIMES ->
"*"
| T T_RPAREN ->
")"
| T T_PLUS ->
"+"
| T T_MINUS ->
"-"
| T T_LPAREN ->
"("
| T T_INT ->
string_of_int v
| N N_expr ->
string_of_int v
| N N_main ->
string_of_int v
| T T_EOL ->
""
| T T_DIV ->
"/"
| T T_error ->
"error"
(* Debugging. *)
let dump env =
Printf.fprintf stderr "Stack height: %d\n%!" (I.length (I.view env));
Printf.fprintf stderr "Stack view:\n%s\n%!" (P.print_env print_element env);
begin match Lazy.force (I.view env) with
| I.Nil ->
()
| I.Cons (I.Element (current, _, _, _), _) ->
Printf.fprintf stderr "Current state: %d\n%!" (Obj.magic current);
let items = I.items current in
Printf.fprintf stderr "#Items: %d\n%!" (List.length items);
List.iter (fun item ->
Printf.fprintf stderr "%s\n%!" (P.print_item item)
) items
end;
print_newline()
(* The loop which drives the parser. At each iteration, we analyze a
result produced by the parser, and act in an appropriate manner. *)
(* [lexbuf] is the lexing buffer. [result] is the last result produced
by the parser. *)
let rec loop lexbuf (result : int I.result) =
match result with
| I.InputNeeded env ->
dump env;
(* The parser needs a token. Request one from the lexer,
and offer it to the parser, which will produce a new
result. Then, repeat. *)
let token = Lexer.token lexbuf in
let startp = lexbuf.Lexing.lex_start_p
and endp = lexbuf.Lexing.lex_curr_p in
let result = I.offer result (token, startp, endp) in
loop lexbuf result
| I.AboutToReduce (env, prod) ->
dump env;
let result = I.resume result in
loop lexbuf result
| I.HandlingError env ->
(* The parser has suspended itself because of a syntax error. Stop. *)
Printf.fprintf stderr
"At offset %d: syntax error.\n%!"
(Lexing.lexeme_start lexbuf)
| I.Accepted v ->
(* The parser has succeeded and produced a semantic value. Print it. *)
Printf.printf "%d\n%!" v
| I.Rejected ->
(* The parser rejects this input. This cannot happen, here, because
we stop as soon as the parser reports [HandlingError]. *)
assert false
(* Initialize the lexer, and catch any exception raised by the lexer. *)
let process (line : string) =
let lexbuf = Lexing.from_string line in
try
loop lexbuf (Parser.Incremental.main())
with
| Lexer.Error msg ->
Printf.fprintf stderr "%s%!" msg
(* The rest of the code is as in the [calc] demo. *)
let process (optional_line : string option) =
match optional_line with
| None ->
()
| Some line ->
process line
let rec repeat channel =
(* Attempt to read one line. *)
let optional_line, continue = Lexer.line channel in
process optional_line;
if continue then
repeat channel
let () =
repeat (Lexing.from_channel stdin)
{
open Parser
exception Error of string
}
(* This rule looks for a single line, terminated with '\n' or eof.
It returns a pair of an optional string (the line that was found)
and a Boolean flag (false if eof was reached). *)
rule line = parse
| ([^'\n']* '\n') as line
(* Normal case: one line, no eof. *)
{ Some line, true }
| eof
(* Normal case: no data, eof. *)
{ None, false }
| ([^'\n']+ as line) eof
(* Special case: some data but missing '\n', then eof.
Consider this as the last line, and add the missing '\n'. *)
{ Some (line ^ "\n"), false }
(* This rule analyzes a single line and turns it into a stream of
tokens. *)
and token = parse
| [' ' '\t']
{ token lexbuf }
| '\n'
{ EOL }
| ['0'-'9']+ as i
{ INT (int_of_string i) }
| '+'
{ PLUS }
| '-'
{ MINUS }
| '*'
{ TIMES }
| '/'
{ DIV }
| '('
{ LPAREN }
| ')'
{ RPAREN }
| _
{ raise (Error (Printf.sprintf "At offset %d: unexpected character.\n" (Lexing.lexeme_start lexbuf))) }
%token <int> INT
%token PLUS MINUS TIMES DIV
%token LPAREN RPAREN
%token EOL
%left PLUS MINUS /* lowest precedence */
%left TIMES DIV /* medium precedence */
%nonassoc UMINUS /* highest precedence */
%start <int> main
%%
main:
| e = expr EOL
{ e }
expr:
| i = INT
{ i }
| LPAREN e = expr RPAREN
{ e }
| e1 = expr PLUS e2 = expr
{ e1 + e2 }
| e1 = expr MINUS e2 = expr
{ e1 - e2 }
| e1 = expr TIMES e2 = expr
{ e1 * e2 }
| e1 = expr DIV e2 = expr
{ e1 / e2 }
| MINUS e = expr %prec UMINUS
{ - e }
*.dvi
*.aux
*.bbl
*.blg
......
......@@ -405,7 +405,10 @@ A declaration of the form:
\dparameter \ocamlparam
\end{quote}
causes the entire parser to become parameterized over the \ocaml module
\nt{uid}, that is, to become an \ocaml functor. If a single specification file
\nt{uid}, that is, to become an \ocaml functor. The directory
\distrib{demos/calc-param} contains a demo that illustrates the use of this switch.
If a single specification file
contains multiple \dparameter declarations, their order is preserved, so that
the module name \nt{uid} introduced by one declaration is effectively in scope
in the declarations that follow. When two \dparameter declarations originate
......@@ -1822,6 +1825,9 @@ access to the lexer. Instead, when the parser needs the next token, it stops
and returns its current state to the user. The user is then responsible for
obtaining this token (typically by invoking the lexer) and resuming the parser
from that state.
%
The directory \distrib{demos/calc-incremental} contains a demo that
illustrates the use of the incremental API.
This API is ``incremental'' in the sense that the user has access to a
sequence of the intermediate states of the parser. Assuming that semantic
......@@ -1949,6 +1955,9 @@ near future.
% TEMPORARY view
% TEMPORARY symbol
% TEMPORARY document the inspection API
% The directory \distrib{demos/calc-inspection} contains a demo that illustrates the use of the inspection API.
% ---------------------------------------------------------------------------------------------------------------------
\section{Coq back-end}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment