Skip to content

Commits on Source 3

# Changes
## 2019/09/24
* Build Menhir's standard library into the Menhir executable instead of
storing it in a separate file `standard.mly`. This removes the need to
hardcode the path to this file into the Menhir executable. This also
removes the need for the command line switch `--stdlib`, which remains
supported but is now ignored, and for the environment variable
`$MENHIR_STDLIB`, which is now ignored. (Suggested and implemented
by Nicolás Ojeda Bär.)
## 2019/06/20
* When compiled with OCaml 4.02.3, Menhir could produce OCaml code
......
......@@ -52,7 +52,6 @@ libdir := $(PREFIX)/share/menhir
mandir := $(PREFIX)/share/man/man1
MANS := doc/menhir.1
DOCS := doc/manual.pdf doc/manual.html doc/manual*.png demos
MLYLIB := src/standard.mly
# ----------------------------------------------------------------------------
......@@ -181,7 +180,6 @@ install:
install $(BUILDDIR)/menhir.$(TARGET) $(bindir)/menhir$(EXE)
# Install Menhir's standard library.
mkdir -p $(libdir)
install -m 644 $(MLYLIB) $(libdir)
# Install MenhirLib and MenhirSdk.
@if `$(BUILDDIR)/menhir.$(TARGET) --suggest-ocamlfind | tr -d '\r'` ; then \
echo 'Installing MenhirLib and MenhirSdk via ocamlfind.' ; \
......@@ -204,7 +202,7 @@ install:
fi
uninstall:
@if `$(bindir)/menhir$(EXE) --suggest-ocamlfind` ; then \
@if `$(bindir)/menhir$(EXE) --suggest-ocamlfind | tr -d '\r'` ; then \
echo 'Un-installing MenhirLib and MenhirSdk via ocamlfind.' ; \
ocamlfind remove menhirLib ; \
ocamlfind remove menhirSdk ; \
......
......@@ -15,11 +15,9 @@ TARBALL=$PACKAGE.tar.gz
# We use a dedicated opam switch where it is permitted to uninstall/reinstall
# Menhir.
CURRENT=`opam switch show`
echo "The current opam switch is $CURRENT. Now switching to test-menhir..."
opam switch test-menhir 2>/dev/null || opam switch create test-menhir 4.07.1
eval $(opam env)
OPAMYES=true opam install ocamlfind ocamlbuild coq
echo "Now switching to test-menhir..."
eval $(opam env --set-switch --switch test-menhir)
OPAMYES=true opam install ocamlfind ocamlbuild coq dune
# Uninstall Menhir if it is installed.
......@@ -59,7 +57,7 @@ mkdir $INSTALL
echo " * Building the demos."
(cd $TEMPDIR/$PACKAGE &&
make MENHIR=$INSTALL/bin/menhir -C demos
make MENHIR=$INSTALL/bin/menhir COQINCLUDES="-R $COQCONTRIB/MenhirLib MenhirLib" -C demos
) > $TEMPDIR/demos.log 2>&1 || (cat $TEMPDIR/demos.log; exit 1)
echo " * Uninstalling."
......@@ -69,8 +67,3 @@ echo " * Uninstalling."
) > $TEMPDIR/uninstall.log 2>&1 || (cat $TEMPDIR/uninstall.log; exit 1)
rm -rf $TEMPDIR
# Move back to the original switch.
echo "Switching back to $CURRENT..."
opam switch $CURRENT
# Changes
## XXXXXXXX
* Fix compatibility with Coq 8.10, and some warnings.
## 2019/06/26
* Fix compatibility with Coq 8.7 and Coq 8.9:
......
......@@ -99,9 +99,9 @@ Module Types(Import Init:AutInit).
T term = last_symb_of_non_init_state s -> lookahead_action term
| Reduce_act: production -> lookahead_action term
| Fail_act: lookahead_action term.
Arguments Shift_act [term].
Arguments Reduce_act [term].
Arguments Fail_act [term].
Arguments Shift_act {term}.
Arguments Reduce_act {term}.
Arguments Fail_act {term}.
Inductive action :=
| Default_reduce_act: production -> action
......
......@@ -14,7 +14,7 @@ SHELL := /usr/bin/env bash
# ROOTDIR (default: `pwd`)
# COQBIN (default: empty)
# COQINCLUDE (default: empty)
# V (default: *.v)
# VV (default: *.v)
# V_AUX (default: undefined/empty)
# SERIOUS (default: 1)
# (if 0, we produce .vio files)
......@@ -35,23 +35,23 @@ ifndef ROOTDIR
ROOTDIR := $(shell pwd)
endif
ifndef V
V := $(wildcard $(ROOTDIR)/*.v)
ifndef VV
VV := $(wildcard $(ROOTDIR)/*.v)
endif
# Typically, $(V) should list only the .v files that we are ultimately
# Typically, $(VV) should list only the .v files that we are ultimately
# interested in checking. $(V_AUX) should list every other .v file in the
# project. $(VD) is obtained from $(V) and $(V_AUX), so [make] sees all
# project. $(VD) is obtained from $(VV) and $(V_AUX), so [make] sees all
# dependencies and can rebuild files anywhere in the project, if needed, and
# only if needed.
ifndef VD
VD := $(patsubst %.v,%.v.d,$(V) $(V_AUX))
VD := $(patsubst %.v,%.v.d,$(VV) $(V_AUX))
endif
VIO := $(patsubst %.v,%.vio,$(V))
VQ := $(patsubst %.v,%.vq,$(V))
VO := $(patsubst %.v,%.vo,$(V))
VIO := $(patsubst %.v,%.vio,$(VV))
VQ := $(patsubst %.v,%.vq,$(VV))
VO := $(patsubst %.v,%.vo,$(VV))
SERIOUS := 1
......@@ -188,7 +188,7 @@ ide: _CoqProject
# In a multi-directory setting, it is not entirely clear how to find the
# files that we wish to remove.
# One approach would be to view $(V) as the authoritative list of source files
# One approach would be to view $(VV) as the authoritative list of source files
# and remove just the derived files $(VO), etc.
# Another approach is to scan all subdirectories of $(ROOTDIR) and remove all
......
......@@ -17,7 +17,7 @@ Require Import Alphabet.
Class IsValidator (P : Prop) (b : bool) :=
is_validator : b = true -> P.
Hint Mode IsValidator + -.
Hint Mode IsValidator + - : typeclass_instances.
Instance is_validator_true : IsValidator True true.
Proof. done. Qed.
......@@ -31,7 +31,7 @@ Proof. done. Qed.
Instance is_validator_and P1 b1 P2 b2 `{IsValidator P1 b1} `{IsValidator P2 b2}:
IsValidator (P1 /\ P2) (if b1 then b2 else false).
Proof. split; destruct b1, b2; auto using is_validator. Qed.
Proof. by split; destruct b1, b2; apply is_validator. Qed.
Instance is_validator_comparable_leibniz_eq A (C:Comparable A) (x y : A) :
ComparableLeibnizEq C ->
......@@ -49,9 +49,10 @@ Lemma is_validator_forall_finite A P b `(Finite A) :
(forall (x : A), IsValidator (P x) (b x)) ->
IsValidator (forall (x : A), P x) (forallb b all_list).
Proof.
move=> ? /forallb_forall.
auto using all_list_forall, is_validator, forallb_forall.
move=> ? /forallb_forall Hb ?.
apply is_validator, Hb, all_list_forall.
Qed.
(* We do not use an instance directly here, because we need somehow to
force Coq to instantiate b with a lambda. *)
Hint Extern 2 (IsValidator (forall x : ?A, _) _) =>
......
......@@ -184,8 +184,8 @@ Instance impl_is_state_valid_after_pop_is_validator state sl pl P b :
IsValidator (state_valid_after_pop state sl pl -> P)
(if is_state_valid_after_pop state sl pl then b else true).
Proof.
destruct (is_state_valid_after_pop state0 sl pl) eqn:EQ.
- intros ??. auto using is_validator.
destruct (is_state_valid_after_pop _ sl pl) eqn:EQ.
- intros ???. by eapply is_validator.
- intros _ _ Hsvap. exfalso. induction Hsvap=>//; [simpl in EQ; congruence|].
by destruct sl.
Qed.
......
......@@ -12,4 +12,4 @@
(****************************************************************************)
Definition require_unreleased := tt.
Definition require_20190626 := tt.
Definition require_20190924 := tt.
menhir (20190924-1) unstable; urgency=medium
* New upstream version
* Set Multi-Arch:foreign for the menhir-doc package
* Standards-Version: 4.4.1 (no change)
-- Ralf Treinen <treinen@debian.org> Sat, 02 Nov 2019 11:51:19 +0100
menhir (20190626-6) unstable; urgency=medium
* Team upload
......
......@@ -12,7 +12,7 @@ Build-Depends:
ocaml-findlib,
dh-ocaml,
coq
Standards-Version: 4.4.0
Standards-Version: 4.4.1
Homepage: http://gallium.inria.fr/~fpottier/menhir/
Vcs-Browser: https://salsa.debian.org/ocaml-team/menhir
Vcs-Git: https://salsa.debian.org/ocaml-team/menhir.git
......@@ -65,6 +65,7 @@ Replaces: menhir (<< 20170712-1)
Breaks: menhir (<< 20170712-1)
Architecture: all
Depends: ${misc:Depends}
Multi-Arch: foreign
Description: Documentation of the Menhir parser generator for OCaml
Menhir is a LR(1) parser generator for the OCaml programming language.
It is mostly compatible with the ocamlyacc parser generator provided with
......
......@@ -28,6 +28,7 @@ DEMOS := \
calc-incremental-dune \
calc-inspection-dune \
generate-printers-dune \
coq-minicalc
.PHONY: all clean test
......
(** Hand-written lexer for natural numbers, idents, parens and + - * / *)
Require Import BinNat Ascii String.
Require Import Parser.
Import MenhirLibParser.Inter.
Open Scope char_scope.
Open Scope bool_scope.
(** No such thing as an empty buffer, instead we use
an infinite stream of EOF *)
CoFixpoint TheEnd : buffer := Buf_cons (EOF tt) TheEnd.
Fixpoint ntail n s :=
match n, s with
| 0, _ => s
| _, EmptyString => s
| S n, String _ s => ntail n s
end.
(** Comparison on characters *)
Definition ascii_eqb c c' := (N_of_ascii c =? N_of_ascii c')%N.
Definition ascii_leb c c' := (N_of_ascii c <=? N_of_ascii c')%N.
Infix "=?" := ascii_eqb : char_scope.
Infix "<=?" := ascii_leb : char_scope.
Definition is_digit c := (("0" <=? c) && (c <=? "9"))%char.
Definition is_alpha c :=
((("a" <=? c) && (c <=? "z")) ||
(("A" <=? c) && (c <=? "Z")) ||
(c =? "_"))%char.
Fixpoint identsize s :=
match s with
| EmptyString => 0
| String c s =>
if is_alpha c || is_digit c then S (identsize s)
else 0
end.
Fixpoint readnum acc s :=
match s with
| String "0" s => readnum (acc*10) s
| String "1" s => readnum (acc*10+1) s
| String "2" s => readnum (acc*10+2) s
| String "3" s => readnum (acc*10+3) s
| String "4" s => readnum (acc*10+4) s
| String "5" s => readnum (acc*10+5) s
| String "6" s => readnum (acc*10+6) s
| String "7" s => readnum (acc*10+7) s
| String "8" s => readnum (acc*10+8) s
| String "9" s => readnum (acc*10+9) s
| _ => (acc,s)
end.
Fixpoint lex_string_cpt n s :=
match n with
| 0 => None
| S n =>
match s with
| EmptyString => Some TheEnd
| String c s' =>
match c with
| " " => lex_string_cpt n s'
| "009" => lex_string_cpt n s' (* \t *)
| "010" => lex_string_cpt n s' (* \n *)
| "013" => lex_string_cpt n s' (* \r *)
| "(" => option_map (Buf_cons (LPAREN tt)) (lex_string_cpt n s')
| ")" => option_map (Buf_cons (RPAREN tt)) (lex_string_cpt n s')
| "+" => option_map (Buf_cons (ADD tt)) (lex_string_cpt n s')
| "-" => option_map (Buf_cons (SUB tt)) (lex_string_cpt n s')
| "*" => option_map (Buf_cons (MUL tt)) (lex_string_cpt n s')
| "/" => option_map (Buf_cons (DIV tt)) (lex_string_cpt n s')
| _ =>
if is_digit c then
let (m,s) := readnum 0 s in
option_map (Buf_cons (NUM m)) (lex_string_cpt n s)
else if is_alpha c then
let k := identsize s in
let id := substring 0 k s in
let s := ntail k s in
option_map (Buf_cons (ID id)) (lex_string_cpt n s)
else None
end
end
end.
Definition lex_string s := lex_string_cpt (length s) s.
MENHIR := menhir
MENHIRFLAGS := --coq
COQINCLUDES :=
Makefile.coq:
coq_makefile -o Makefile.coq Lexer.v MiniCalc.v Parser.v $(COQINCLUDES)
Parser.v : Parser.vy
$(MENHIR) $(MENHIRFLAGS) $<
include Makefile.coq
clean::
rm -f Parser.v
rm -f Makefile.coq Makefile.coq.conf
rm -f .*.aux
Require Import Parser Lexer List String PeanoNat.
Import MenhirLibParser.Inter.
Import ListNotations.
Open Scope string_scope.
(** Lexer + Parser for little arithmetic expressions *)
Definition string2expr s :=
match option_map (Parser.parse_expr 50) (Lexer.lex_string s) with
| Some (Parsed_pr f _) => Some f
| _ => None
end.
(** Let's print back our little expressions *)
Module Print.
Definition pr_digit n :=
match n with
| 0 => "0"
| 1 => "1"
| 2 => "2"
| 3 => "3"
| 4 => "4"
| 5 => "5"
| 6 => "6"
| 7 => "7"
| 8 => "8"
| _ => "9"
end.
Fixpoint prnat_loop n k :=
match k with
| 0 => ""
| S k =>
match n/10 with
| 0 => pr_digit n
| q => prnat_loop q k ++ pr_digit (n mod 10)
end
end.
Definition prnat n := prnat_loop n (S n).
Fixpoint pr_expr e :=
match e with
| Ast.Num n => prnat n
| Ast.Var x => x
| Ast.Add e e' => "(" ++ pr_expr e ++ "+" ++ pr_expr e' ++ ")"
| Ast.Sub e e' => "(" ++ pr_expr e ++ "-" ++ pr_expr e' ++ ")"
| Ast.Mul e e' => "(" ++ pr_expr e ++ "*" ++ pr_expr e' ++ ")"
| Ast.Div e e' => "(" ++ pr_expr e ++ "/" ++ pr_expr e' ++ ")"
end.
End Print.
Definition example := "12 + 34*x / (48+y)".
Definition expected_reprint := "(12+((34*x)/(48+y)))".
Compute option_map Print.pr_expr (string2expr example).
Definition check :=
match option_map Print.pr_expr (string2expr example) with
| Some s => if string_dec s expected_reprint then "OK" else "KO"
| None => "KO"
end.
(** This should display "OK" *)
Compute check.
(* Grammar for little arithmetic expressions (+-*/) *)
%{
Require Import String.
Module Ast.
Inductive expr :=
| Var : string -> expr
| Num : nat -> expr
| Add : expr -> expr -> expr
| Sub : expr -> expr -> expr
| Mul : expr -> expr -> expr
| Div : expr -> expr -> expr.
End Ast.
%}
%token ADD SUB MUL DIV LPAREN RPAREN EOF
%token<nat> NUM
%token<string> ID
%start<Ast.expr> parse_expr
%type<Ast.expr> p_expr
%type<Ast.expr> p_factor
%type<Ast.expr> p_atom
%%
parse_expr : p_expr EOF { $1 }
p_atom :
ID { Ast.Var $1 }
| NUM { Ast.Num $1 }
| LPAREN p_expr RPAREN { $2 }
p_expr :
| p_factor { $1 }
| p_expr ADD p_factor { Ast.Add $1 $3 }
| p_expr SUB p_factor { Ast.Sub $1 $3 }
p_factor :
| p_atom { $1 }
| p_factor MUL p_atom { Ast.Mul $1 $3 }
| p_factor DIV p_atom { Ast.Div $1 $3 }
Coq-MiniCalc : a little demo of Lexing/Parsing in Coq
=====================================================
Pierre Letouzey, 2019
Licence : CC0
This is a toy demo of the recent Coq backend of `menhir`.
This micro-grammar recognizes arithmetic expressions : numbers, idents, `+` `*` `-` `/` and parenthesis.
We provide an hand-written lexer, and a minimal final test (compilation should display "OK").
Tested with Coq 8.8 + menhir 2019/06/13 + corresponding coq-menhirlib.
Anything more recent than that should be ok.
\ No newline at end of file
-I .
-R . MiniCalc
Parser.v
Lexer.v
MiniCalc.v
......@@ -58,13 +58,13 @@ font-size: 1rem;
}
</style>
<title>Menhir Reference Manual
(version 20190626)
(version 20190924)
</title>
</head>
<body >
<!--HEVEA command line is: hevea -fix manual.tex -->
<!--CUT STYLE article--><!--CUT DEF section 1 --><table class="title"><tr><td style="padding:1ex"><h1 class="titlemain">Menhir Reference Manual<br>
(version 20190626)</h1><h3 class="titlerest">François Pottier and Yann Régis-Gianas<br>
(version 20190924)</h1><h3 class="titlerest">François Pottier and Yann Régis-Gianas<br>
INRIA<br>
<span style="font-family:monospace">{Francois.Pottier, Yann.Regis-Gianas}@inria.fr</span></h3></td></tr>
</table><!--TOC section id="sec1" Contents-->
......@@ -281,10 +281,8 @@ which is printed on the standard output channel.</p><p><span style="font-family:
the grammar specification to be translated into a definition of the <span style="font-family:monospace">token</span> type, which is written to the files <span style="font-style:italic">basename</span><span style="font-family:monospace">.ml</span> and
<span style="font-style:italic">basename</span><span style="font-family:monospace">.mli</span>. No code is generated. This is useful when
a single set of tokens is to be shared between several parsers. The directory
<a href="https://gitlab.inria.fr/fpottier/menhir/blob/master/demos/calc-two"><span style="font-family:monospace">demos/calc-two</span></a> contains a demo that illustrates the use of this switch.</p><p><span style="font-family:monospace">--raw-depend</span>. See §<a href="#sec%3Abuild">14</a>.</p><p><span style="font-family:monospace">--stdlib</span> <span style="font-style:italic">directory</span>. This switch controls the directory where
the standard library (§<a href="#sec%3Alibrary">5.4</a>) is found. It takes precedence over
both the installation-time directory and the directory that may be specified
via the environment variable <code>$MENHIR_STDLIB</code>.</p><p><span style="font-family:monospace">--strict</span>. This switch causes several warnings about the grammar
<a href="https://gitlab.inria.fr/fpottier/menhir/blob/master/demos/calc-two"><span style="font-family:monospace">demos/calc-two</span></a> contains a demo that illustrates the use of this switch.</p><p><span style="font-family:monospace">--raw-depend</span>. See §<a href="#sec%3Abuild">14</a>.</p><p><span style="font-family:monospace">--stdlib</span> <span style="font-style:italic">directory</span>. This switch exists only for
backwards compatibility and is ignored. It may be removed in the future.</p><p><span style="font-family:monospace">--strict</span>. This switch causes several warnings about the grammar
and about the automaton to be considered errors. This includes warnings about
useless precedence declarations, non-terminal symbols that produce the empty
language, unreachable non-terminal symbols, productions that are never
......@@ -1130,13 +1128,7 @@ more elaborate notions. For instance, the following rule:
causes <span style="font-style:italic">plist</span>(<span style="font-style:italic">X</span>) to recognize a list of <span style="font-style:italic">X</span>’s, where the empty
list is represented by the empty string, and a non-empty list is delimited
with parentheses and comma-separated.</p><p>The standard library is stored in a file named <a href="https://gitlab.inria.fr/fpottier/menhir/blob/master/src/standard.mly"><span style="font-family:monospace">standard.mly</span></a>, which is
installed at the same time as Menhir. By default, Menhir attempts to find this
file in the directory where this file was installed. This can be overridden by
setting the environment variable
<code>$MENHIR_STDLIB</code>. If defined, this variable should contain the path of
the directory where <span style="font-family:monospace">standard.mly</span> is stored. (This path may
end with a <span style="font-family:monospace">/</span> character.) This can be overridden also via the
command line switch <span style="font-family:monospace">--stdlib</span>.
embedded inside Menhir when it is built.
The command line switch <span style="font-family:monospace">--no-stdlib</span> instructs Menhir to <em>not</em> load the
standard library.</p><p>The meaning of the symbols defined in the standard library
(Figure <a href="#fig%3Astandard">3</a>) should be clear in most cases. Yet, the
......
No preview for this file type