Commit 33561435 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge ../coq-menhirlib

parents eb2b1ff7 08374566
# Changes
## 2018/08/27
* Avoid an undocumented mode of use of the `fix` tactic,
which would cause an incompatibility with Coq > 8.8.1.
(Reported and corrected by Michael Soegtrop.)
## 2018/05/30
* Initial release.
# -------------------------------------------------------------------------
# Private Makefile for package maintenance.
SHELL := bash
export CDPATH=
.PHONY: package export opam submit pin unpin
# -------------------------------------------------------------------------
include Makefile
# -------------------------------------------------------------------------
# Distribution.
# The version number is automatically set to the current date,
# unless DATE is defined on the command line.
DATE := $(shell /bin/date +%Y%m%d)
# The project name on gitlab.
PROJECT := coq-menhirlib
# The opam package name.
PACKAGE := coq-menhirlib
# The repository URL (https).
REPO := https://gitlab.inria.fr/fpottier/$(PROJECT)
# The archive URL (https).
ARCHIVE := $(REPO)/repository/$(DATE)/archive.tar.gz
# The local repository directory.
PWD := $(shell pwd)
# -------------------------------------------------------------------------
# Prepare a release.
package:
# Make sure the correct version can be installed.
@ make uninstall
@ make clean
@ make install
# -------------------------------------------------------------------------
# Publish a release. (Remember to commit everything first!)
export:
# Check if everything has been committed.
@ if [ -n "$$(git status --porcelain)" ] ; then \
echo "Error: there remain uncommitted changes." ; \
git status ; \
exit 1 ; \
else \
echo "Now making a release..." ; \
fi
# Create a git tag.
@ git tag -a $(DATE) -m "Release $(DATE)."
# Upload. (This automatically makes a .tar.gz archive available on gitlab.)
@ git push
@ git push --tags
# -------------------------------------------------------------------------
# Updating the opam package.
# This entry assumes that "make package" and "make export"
# have just been run (on the same day).
# You need opam-publish:
# sudo apt-get install libssl-dev
# opam install tls opam-publish
# In fact, you need a version of opam-publish that supports --subdirectory:
# git clone git@github.com:fpottier/opam-publish.git
# cd opam-publish
# git checkout 1.3
# opam pin add opam-publish `pwd` -k git
# The following command should have been run once:
# opam-publish repo add opam-coq-archive coq/opam-coq-archive
PUBLISH_OPTIONS := \
--repo opam-coq-archive \
--subdirectory released \
opam:
@ opam lint
@ opam-publish prepare $(PUBLISH_OPTIONS) $(PACKAGE).$(DATE) $(ARCHIVE)
submit:
@ opam-publish submit $(PUBLISH_OPTIONS) $(PACKAGE).$(DATE)
# -------------------------------------------------------------------------
# Pinning.
pin:
opam pin add $(PACKAGE) `pwd` -k git
unpin:
opam pin remove $(PACKAGE)
GNU LESSER GENERAL PUBLIC LICENSE
Version 3, 29 June 2007
Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>
Everyone is permitted to copy and distribute verbatim copies
of this license document, but changing it is not allowed.
This version of the GNU Lesser General Public License incorporates
the terms and conditions of version 3 of the GNU General Public
License, supplemented by the additional permissions listed below.
0. Additional Definitions.
As used herein, "this License" refers to version 3 of the GNU Lesser
General Public License, and the "GNU GPL" refers to version 3 of the GNU
General Public License.
"The Library" refers to a covered work governed by this License,
other than an Application or a Combined Work as defined below.
An "Application" is any work that makes use of an interface provided
by the Library, but which is not otherwise based on the Library.
Defining a subclass of a class defined by the Library is deemed a mode
of using an interface provided by the Library.
A "Combined Work" is a work produced by combining or linking an
Application with the Library. The particular version of the Library
with which the Combined Work was made is also called the "Linked
Version".
The "Minimal Corresponding Source" for a Combined Work means the
Corresponding Source for the Combined Work, excluding any source code
for portions of the Combined Work that, considered in isolation, are
based on the Application, and not on the Linked Version.
The "Corresponding Application Code" for a Combined Work means the
object code and/or source code for the Application, including any data
and utility programs needed for reproducing the Combined Work from the
Application, but excluding the System Libraries of the Combined Work.
1. Exception to Section 3 of the GNU GPL.
You may convey a covered work under sections 3 and 4 of this License
without being bound by section 3 of the GNU GPL.
2. Conveying Modified Versions.
If you modify a copy of the Library, and, in your modifications, a
facility refers to a function or data to be supplied by an Application
that uses the facility (other than as an argument passed when the
facility is invoked), then you may convey a copy of the modified
version:
a) under this License, provided that you make a good faith effort to
ensure that, in the event an Application does not supply the
function or data, the facility still operates, and performs
whatever part of its purpose remains meaningful, or
b) under the GNU GPL, with none of the additional permissions of
this License applicable to that copy.
3. Object Code Incorporating Material from Library Header Files.
The object code form of an Application may incorporate material from
a header file that is part of the Library. You may convey such object
code under terms of your choice, provided that, if the incorporated
material is not limited to numerical parameters, data structure
layouts and accessors, or small macros, inline functions and templates
(ten or fewer lines in length), you do both of the following:
a) Give prominent notice with each copy of the object code that the
Library is used in it and that the Library and its use are
covered by this License.
b) Accompany the object code with a copy of the GNU GPL and this license
document.
4. Combined Works.
You may convey a Combined Work under terms of your choice that,
taken together, effectively do not restrict modification of the
portions of the Library contained in the Combined Work and reverse
engineering for debugging such modifications, if you also do each of
the following:
a) Give prominent notice with each copy of the Combined Work that
the Library is used in it and that the Library and its use are
covered by this License.
b) Accompany the Combined Work with a copy of the GNU GPL and this license
document.
c) For a Combined Work that displays copyright notices during
execution, include the copyright notice for the Library among
these notices, as well as a reference directing the user to the
copies of the GNU GPL and this license document.
d) Do one of the following:
0) Convey the Minimal Corresponding Source under the terms of this
License, and the Corresponding Application Code in a form
suitable for, and under terms that permit, the user to
recombine or relink the Application with a modified version of
the Linked Version to produce a modified Combined Work, in the
manner specified by section 6 of the GNU GPL for conveying
Corresponding Source.
1) Use a suitable shared library mechanism for linking with the
Library. A suitable mechanism is one that (a) uses at run time
a copy of the Library already present on the user's computer
system, and (b) will operate properly with a modified version
of the Library that is interface-compatible with the Linked
Version.
e) Provide Installation Information, but only if you would otherwise
be required to provide such information under section 6 of the
GNU GPL, and only to the extent that such information is
necessary to install and execute a modified version of the
Combined Work produced by recombining or relinking the
Application with a modified version of the Linked Version. (If
you use option 4d0, the Installation Information must accompany
the Minimal Corresponding Source and Corresponding Application
Code. If you use option 4d1, you must provide the Installation
Information in the manner specified by section 6 of the GNU GPL
for conveying Corresponding Source.)
5. Combined Libraries.
You may place library facilities that are a work based on the
Library side by side in a single library together with other library
facilities that are not Applications and are not covered by this
License, and convey such a combined library under terms of your
choice, if you do both of the following:
a) Accompany the combined library with a copy of the same work based
on the Library, uncombined with any other library facilities,
conveyed under the terms of this License.
b) Give prominent notice with the combined library that part of it
is a work based on the Library, and explaining where to find the
accompanying uncombined form of the same work.
6. Revised Versions of the GNU Lesser General Public License.
The Free Software Foundation may publish revised and/or new versions
of the GNU Lesser General Public License from time to time. Such new
versions will be similar in spirit to the present version, but may
differ in detail to address new problems or concerns.
Each version is given a distinguishing version number. If the
Library as you received it specifies that a certain numbered version
of the GNU Lesser General Public License "or any later version"
applies to it, you have the option of following the terms and
conditions either of that published version or of any later version
published by the Free Software Foundation. If the Library as you
received it does not specify a version number of the GNU Lesser
General Public License, you may choose any version of the GNU Lesser
General Public License ever published by the Free Software Foundation.
If the Library as you received it specifies that a proxy can decide
whether future versions of the GNU Lesser General Public License shall
apply, that proxy's public statement of acceptance of any version is
permanent authorization for you to choose that version for the
Library.
# Delegate the following commands:
.PHONY: all clean install uninstall
all clean install uninstall:
@ $(MAKE) -C src --no-print-directory $@
# A support library for verified Coq parsers produced by Menhir
The [Menhir](http://gallium.inria.fr/~fpottier/menhir/) parser generator,
in `--coq` mode, can produce [Coq](https://coq.inria.fr/) parsers.
These parsers must be linked against this library, which provides
both an interpreter (which allows running the generated parser) and
a validator (which allows verifying, at parser construction time,
that the generated parser is correct and complete with respect to
the grammar).
## Installation
To install the latest released version, use `opam install coq-menhirlib`.
To install from the sources, use `make` followed with `make install`.
## Authors
* [Jacques-Henri Jourdan](jacques-henri.jourdan@lri.fr)
A support library for verified Coq parsers produced by Menhir
The Menhir parser generator, in --coq mode, can produce Coq parsers.
These parsers must be linked against this library, which provides
both an interpreter (which allows running the generated parser) and
a validator (which allows verifying, at parser construction time,
that the generated parser is correct and complete with respect to
the grammar).
name: "coq-menhirlib"
opam-version: "1.2"
synopsis: "A support library for verified Coq parsers produced by Menhir"
maintainer: "francois.pottier@inria.fr"
authors: [
"Jacques-Henri Jourdan <jacques-henri.jourdan@lri.fr>"
]
homepage: "https://gitlab.inria.fr/fpottier/coq-menhirlib"
dev-repo: "https://gitlab.inria.fr/fpottier/coq-menhirlib.git"
bug-reports: "jacques-henri.jourdan@lri.fr"
build: [
[make "-j%{jobs}%"]
]
install: [
[make "install"]
]
remove: [
[make "uninstall"]
]
depends: [
"coq" { >= "8.6" }
]
conflicts: [
"menhir" { < "20180530" }
]
*.vo
*.glob
*.v.d
.*.aux
_CoqProject
This diff is collapsed.
(* *********************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 3 of *)
(* the License, or (at your option) any later version. *)
(* *)
(* *********************************************************************)
From MenhirLib Require Grammar.
From MenhirLib Require Export Alphabet.
From Coq Require Import Orders.
From Coq Require Export List Syntax.
Module Type AutInit.
(** The grammar of the automaton. **)
Declare Module Gram:Grammar.T.
Export Gram.
(** The set of non initial state is considered as an alphabet. **)
Parameter noninitstate : Type.
Declare Instance NonInitStateAlph : Alphabet noninitstate.
Parameter initstate : Type.
Declare Instance InitStateAlph : Alphabet initstate.
(** When we are at this state, we know that this symbol is the top of the
stack. **)
Parameter last_symb_of_non_init_state: noninitstate -> symbol.
End AutInit.
Module Types(Import Init:AutInit).
(** In many ways, the behaviour of the initial state is different from the
behaviour of the other states. So we have chosen to explicitaly separate
them: the user has to provide the type of non initial states. **)
Inductive state :=
| Init: initstate -> state
| Ninit: noninitstate -> state.
Program Instance StateAlph : Alphabet state :=
{ AlphabetComparable := {| compare := fun x y =>
match x, y return comparison with
| Init _, Ninit _ => Lt
| Init x, Init y => compare x y
| Ninit _, Init _ => Gt
| Ninit x, Ninit y => compare x y
end |};
AlphabetFinite := {| all_list := map Init all_list ++ map Ninit all_list |} }.
Local Obligation Tactic := intros.
Next Obligation.
destruct x, y; intuition; apply compare_antisym.
Qed.
Next Obligation.
destruct x, y, z; intuition.
apply (compare_trans _ i0); intuition.
congruence.
congruence.
apply (compare_trans _ n0); intuition.
Qed.
Next Obligation.
intros x y.
destruct x, y; intuition; try discriminate.
rewrite (compare_eq i i0); intuition.
rewrite (compare_eq n n0); intuition.
Qed.
Next Obligation.
apply in_or_app; destruct x; intuition;
[left|right]; apply in_map; apply all_list_forall.
Qed.
Coercion Ninit : noninitstate >-> state.
Coercion Init : initstate >-> state.
(** For an LR automaton, there are four kind of actions that can be done at a
given state:
- Shifting, that is reading a token and putting it into the stack,
- Reducing a production, that is popping the right hand side of the
production from the stack, and pushing the left hand side,
- Failing
- Accepting the word (special case of reduction)
As in the menhir parser generator, we do not want our parser to read after
the end of stream. That means that once the parser has read a word in the
grammar language, it should stop without peeking the input stream. So, for
the automaton to be complete, the grammar must be particular: if a word is
in its language, then it is not a prefix of an other word of the language
(otherwise, menhir reports an end of stream conflict).
As a consequence of that, there is two notions of action: the first one is
an action performed before having read the stream, the second one is after
**)
Inductive lookahead_action (term:terminal) :=
| Shift_act: forall s:noninitstate,
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].
Inductive action :=
| Default_reduce_act: production -> action
| Lookahead_act : (forall term:terminal, lookahead_action term) -> action.
(** Types used for the annotations of the automaton. **)
(** An item is a part of the annotations given to the validator.
It is acually a set of LR(1) items sharing the same core. It is needed
to validate completeness. **)
Record item := {
(** The pseudo-production of the item. **)
prod_item: production;
(** The position of the dot. **)
dot_pos_item: nat;
(** The lookahead symbol of the item. We are using a list, so we can store
together multiple LR(1) items sharing the same core. **)
lookaheads_item: list terminal
}.
End Types.
Module Type T.
Include AutInit <+ Types.
Module Export GramDefs := Grammar.Defs Gram.
(** For each initial state, the non terminal it recognizes. **)
Parameter start_nt: initstate -> nonterminal.
(** The action table maps a state to either a map terminal -> action. **)
Parameter action_table:
state -> action.
(** The goto table of an LR(1) automaton. **)
Parameter goto_table: state -> forall nt:nonterminal,
option { s:noninitstate | NT nt = last_symb_of_non_init_state s }.
(** Some annotations on the automaton to help the validation. **)
(** When we are at this state, we know that these symbols are just below
the top of the stack. The list is ordered such that the head correspond
to the (almost) top of the stack. **)
Parameter past_symb_of_non_init_state: noninitstate -> list symbol.
(** When we are at this state, the (strictly) previous states verify these
predicates. **)
Parameter past_state_of_non_init_state: noninitstate -> list (state -> bool).
(** The items of the state. **)
Parameter items_of_state: state -> list item.
(** The nullable predicate for non terminals :
true if and only if the symbol produces the empty string **)
Parameter nullable_nterm: nonterminal -> bool.
(** The first predicates for non terminals, symbols or words of symbols. A
terminal is in the returned list if, and only if the parameter produces a
word that begins with the given terminal **)
Parameter first_nterm: nonterminal -> list terminal.
End T.
(* *********************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 3 of *)
(* the License, or (at your option) any later version. *)
(* *)
(* *********************************************************************)
From Coq Require Import List Syntax Orders.
From MenhirLib Require Import Alphabet.
(** The terminal non-terminal alphabets of the grammar. **)
Module Type Alphs.
Parameters terminal nonterminal : Type.
Declare Instance TerminalAlph: Alphabet terminal.
Declare Instance NonTerminalAlph: Alphabet nonterminal.
End Alphs.
(** Definition of the alphabet of symbols, given the alphabet of terminals
and the alphabet of non terminals **)
Module Symbol(Import A:Alphs).
Inductive symbol :=
| T: terminal -> symbol
| NT: nonterminal -> symbol.
Program Instance SymbolAlph : Alphabet symbol :=
{ AlphabetComparable := {| compare := fun x y =>
match x, y return comparison with
| T _, NT _ => Gt
| NT _, T _ => Lt
| T x, T y => compare x y
| NT x, NT y => compare x y
end |};
AlphabetFinite := {| all_list :=
map T all_list++map NT all_list |} }.
Next Obligation.
destruct x; destruct y; intuition; apply compare_antisym.
Qed.
Next Obligation.
destruct x; destruct y; destruct z; intuition; try discriminate.
apply (compare_trans _ t0); intuition.
apply (compare_trans _ n0); intuition.
Qed.
Next Obligation.
intros x y.
destruct x; destruct y; try discriminate; intros.
rewrite (compare_eq t t0); intuition.
rewrite (compare_eq n n0); intuition.
Qed.
Next Obligation.
rewrite in_app_iff.
destruct x; [left | right]; apply in_map; apply all_list_forall.
Qed.
End Symbol.
(** A curryfied function with multiple parameters **)
Definition arrows_right: Type -> list Type -> Type :=
fold_right (fun A B => A -> B).
Module Type T.
Include Alphs <+ Symbol.
(** [symbol_semantic_type] maps a symbols to the type of its semantic
values. **)
Parameter symbol_semantic_type: symbol -> Type.
(** The type of productions identifiers **)
Parameter production : Type.
Declare Instance ProductionAlph : Alphabet production.
(** Accessors for productions: left hand side, right hand side,
and semantic action. The semantic actions are given in the form
of curryfied functions, that take arguments in the reverse order. **)
Parameter prod_lhs: production -> nonterminal.
(* The RHS of a production is given in reversed order, so that symbols *)
Parameter prod_rhs_rev: production -> list symbol.
Parameter prod_action:
forall p:production,
arrows_right
(symbol_semantic_type (NT (prod_lhs p)))
(map symbol_semantic_type (prod_rhs_rev p)).
End T.
Module Defs(Import G:T).
(** A token is a terminal and a semantic value for this terminal. **)
Definition token := {t:terminal & symbol_semantic_type (T t)}.
(** The semantics of a grammar is defined in two stages. First, we
define the notion of parse tree, which represents one way of
recognizing a word with a head symbol. Semantic values are stored
at the leaves.
This notion is defined in two mutually recursive flavours:
either for a single head symbol, or for a list of head symbols. *)
Inductive parse_tree:
forall (head_symbol:symbol) (word:list token), Type :=
(** Parse tree for a terminal symbol. *)
| Terminal_pt:
forall (t:terminal) (sem:symbol_semantic_type (T t)),
parse_tree (T t) [existT (fun t => symbol_semantic_type (T t)) t sem]
(** Parse tree for a non-terminal symbol. *)
| Non_terminal_pt:
forall (prod:production) {word:list token},
parse_tree_list (prod_rhs_rev prod) word ->
parse_tree (NT (prod_lhs prod)) word
(* Note : the list head_symbols_rev is reversed. *)
with parse_tree_list:
forall (head_symbols_rev:list symbol) (word:list token), Type :=
| Nil_ptl: parse_tree_list [] []
| Cons_ptl:
forall {head_symbolsq:list symbol} {wordq:list token},
parse_tree_list head_symbolsq wordq ->
forall {head_symbolt:symbol} {wordt:list token},
parse_tree head_symbolt wordt ->
parse_tree_list (head_symbolt::head_symbolsq) (wordq++wordt).
(** We can now finish the definition of the semantics of a grammar,
by giving the semantic value assotiated with a parse tree. *)
Fixpoint pt_sem {head_symbol word} (tree:parse_tree head_symbol word) :
symbol_semantic_type head_symbol :=
match tree with
| Terminal_pt _ sem => sem
| Non_terminal_pt prod ptl => ptl_sem ptl (prod_action prod)
end
with ptl_sem {A head_symbols word} (tree:parse_tree_list head_symbols word) :
arrows_right A (map symbol_semantic_type head_symbols) -> A :=
match tree with
| Nil_ptl => fun act => act
| Cons_ptl q t => fun act => ptl_sem q (act (pt_sem t))
end.
Fixpoint pt_size {head_symbol word} (tree:parse_tree head_symbol word) :=
match tree with
| Terminal_pt _ _ => 1
| Non_terminal_pt _ l => S (ptl_size l)
end
with ptl_size {head_symbols word} (tree:parse_tree_list head_symbols word) :=
match tree with
| Nil_ptl => 0
| Cons_ptl q t =>
pt_size t + ptl_size q
end.
End Defs.
This diff is collapsed.
This diff is collapsed.
(* *********************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 3 of *)
(* the License, or (at your option) any later version. *)
(* *)
(* *********************************************************************)
From Coq Require Import Streams List Syntax.
From MenhirLib Require Import Alphabet.
From MenhirLib Require Grammar Automaton Interpreter.
From Coq.ssr Require Import ssreflect.
Module Make(Import A:Automaton.T) (Import Inter:Interpreter.T A).
(** * Correctness of the interpreter **)
(** We prove that, in any case, if the interpreter accepts returning a
semantic value, then this is a semantic value of the input **)
Section Init.
Variable init:initstate.
(** [word_has_stack_semantics] relates a word with a stack, stating that the
word is a concatenation of words that have the semantic values stored in
the stack. **)
Inductive word_has_stack_semantics:
forall (word:list token) (stack:stack), Prop :=
| Nil_stack_whss: word_has_stack_semantics [] []
| Cons_stack_whss:
forall (wordq:list token) (stackq:stack),
word_has_stack_semantics wordq stackq ->
forall (wordt:list token) (s:noninitstate)