Coq sources, Makefiles, opam package configuration.

.gitignore

+*~

GNUmakefile

+# -------------------------------------------------------------------------
+
+# 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   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)

Makefile

+# Delegate the following commands:
+
+.PHONY: all clean install uninstall
+
+all clean install uninstall:
+	@ $(MAKE) -C src --no-print-directory $@

opam

+name: "coq-menhirlib"
+opam-version: "1.2"
+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" }
+]

src/.gitignore

+*.vo
+*.glob
+*.v.d
+.*.aux
+_CoqProject

src/Alphabet.v

+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          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 General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+From Coq Require Import Int31 Cyclic31 Omega List Syntax
+                        Relations RelationClasses.
+
+Local Obligation Tactic := intros.
+
+(** A comparable type is equiped with a [compare] function, that define an order
+   relation. **)
+Class Comparable (A:Type) := {
+  compare : A -> A -> comparison;
+  compare_antisym : forall x y, CompOpp (compare x y) = compare y x;
+  compare_trans :  forall x y z c,
+    (compare x y) = c -> (compare y z) = c -> (compare x z) = c
+}.
+
+Theorem compare_refl {A:Type} (C: Comparable A) :
+  forall x, compare x x = Eq.
+Proof.
+intros.
+pose proof (compare_antisym x x).
+destruct (compare x x); intuition; try discriminate.
+Qed.
+
+(** The corresponding order is a strict order. **)
+Definition comparableLt {A:Type} (C: Comparable A) : relation A :=
+  fun x y => compare x y = Lt.
+
+Instance ComparableLtStrictOrder {A:Type} (C: Comparable A) :
+  StrictOrder (comparableLt C).
+Proof.
+apply Build_StrictOrder.
+unfold Irreflexive, Reflexive, complement, comparableLt.
+intros.
+pose proof H.
+rewrite <- compare_antisym in H.
+rewrite H0 in H.
+discriminate H.
+unfold Transitive, comparableLt.
+intros x y z.
+apply compare_trans.
+Qed.
+
+(** nat is comparable. **)
+Program Instance natComparable : Comparable nat :=
+  { compare := Nat.compare }.
+Next Obligation.
+symmetry.
+destruct (Nat.compare x y)  as [] eqn:?.
+rewrite Nat.compare_eq_iff in Heqc.
+destruct Heqc.
+rewrite Nat.compare_eq_iff.
+trivial.
+rewrite <- nat_compare_lt in *.
+rewrite <- nat_compare_gt in *.
+trivial.
+rewrite <- nat_compare_lt in *.
+rewrite <- nat_compare_gt in *.
+trivial.
+Qed.
+Next Obligation.
+destruct c.
+rewrite Nat.compare_eq_iff in *; destruct H; assumption.
+rewrite <- nat_compare_lt in *.
+apply (Nat.lt_trans _ _ _ H H0).
+rewrite <- nat_compare_gt in *.
+apply (gt_trans _ _ _ H H0).
+Qed.
+
+(** A pair of comparable is comparable. **)
+Program Instance PairComparable {A:Type} (CA:Comparable A) {B:Type} (CB:Comparable B) :
+  Comparable (A*B) :=
+  { compare := fun x y =>
+      let (xa, xb) := x in let (ya, yb) := y in
+      match compare xa ya return comparison with
+        | Eq => compare xb yb
+        | x => x
+      end }.
+Next Obligation.
+destruct x, y.
+rewrite <- (compare_antisym a a0).
+rewrite <- (compare_antisym b b0).
+destruct (compare a a0); intuition.
+Qed.
+Next Obligation.
+destruct x, y, z.
+destruct (compare a a0) as [] eqn:?, (compare a0 a1) as [] eqn:?;
+try (rewrite <- H0 in H; discriminate);
+try (destruct (compare a a1) as [] eqn:?;
+  try (rewrite <- compare_antisym in Heqc0;
+         rewrite CompOpp_iff in Heqc0;
+         rewrite (compare_trans _ _ _  _ Heqc0 Heqc2) in Heqc1;
+         discriminate);
+  try (rewrite <- compare_antisym in Heqc1;
+         rewrite CompOpp_iff in Heqc1;
+         rewrite (compare_trans _ _ _ _ Heqc2 Heqc1) in Heqc0;
+         discriminate);
+  assumption);
+rewrite (compare_trans _ _ _ _ Heqc0 Heqc1);
+try assumption.
+apply (compare_trans _ _ _ _ H H0).
+Qed.
+
+(** Special case of comparable, where equality is usual equality. **)
+Class ComparableUsualEq {A:Type} (C: Comparable A) :=
+  compare_eq : forall x y, compare x y = Eq -> x = y.
+
+(** Boolean equality for a [Comparable]. **)
+Definition compare_eqb {A:Type} {C:Comparable A} (x y:A) :=
+  match compare x y with
+    | Eq => true
+    | _ => false
+  end.
+
+Theorem compare_eqb_iff {A:Type} {C:Comparable A} {U:ComparableUsualEq C} :
+  forall x y, compare_eqb x y = true <-> x = y.
+Proof.
+unfold compare_eqb.
+intuition.
+apply compare_eq.
+destruct (compare x y); intuition; discriminate.
+destruct H.
+rewrite compare_refl; intuition.
+Qed.
+
+(** [Comparable] provides a decidable equality. **)
+Definition compare_eqdec {A:Type} {C:Comparable A} {U:ComparableUsualEq C} (x y:A):
+  {x = y} + {x <> y}.
+Proof.
+destruct (compare x y) as [] eqn:?; [left; apply compare_eq; intuition | ..];
+  right; intro; destruct H; rewrite compare_refl in Heqc; discriminate.
+Defined.
+
+Instance NComparableUsualEq : ComparableUsualEq natComparable := Nat.compare_eq.
+
+(** A pair of ComparableUsualEq is ComparableUsualEq **)
+Instance PairComparableUsualEq
+  {A:Type} {CA:Comparable A} (UA:ComparableUsualEq CA)
+  {B:Type} {CB:Comparable B} (UB:ComparableUsualEq CB) :
+    ComparableUsualEq (PairComparable CA CB).
+Proof.
+intros x y; destruct x, y; simpl.
+pose proof (compare_eq a a0); pose proof (compare_eq b b0).
+destruct (compare a a0); try discriminate.
+intuition.
+destruct H2, H0.
+reflexivity.
+Qed.
+
+(** An [Finite] type is a type with the list of all elements. **)
+Class Finite (A:Type) := {
+  all_list : list A;
+  all_list_forall : forall x:A, In x all_list
+}.
+
+(** An alphabet is both [ComparableUsualEq] and [Finite]. **)
+Class Alphabet (A:Type) := {
+  AlphabetComparable :> Comparable A;
+  AlphabetComparableUsualEq :> ComparableUsualEq AlphabetComparable;
+  AlphabetFinite :> Finite A
+}.
+
+(** The [Numbered] class provides a conveniant way to build [Alphabet] instances,
+   with a good computationnal complexity. It is mainly a injection from it to
+   [Int31] **)
+Class Numbered (A:Type) := {
+  inj : A -> int31;
+  surj : int31 -> A;
+  surj_inj_compat : forall x, surj (inj x) = x;
+  inj_bound : int31;
+  inj_bound_spec : forall x, (phi (inj x) < phi inj_bound)%Z
+}.
+
+Program Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A :=
+  { AlphabetComparable :=
+      {| compare := fun x y => compare31 (inj x) (inj y) |};
+    AlphabetFinite :=
+      {| all_list := fst (iter_int31 inj_bound _
+        (fun p => (cons (surj (snd p)) (fst p), incr (snd p))) ([], 0%int31)) |} }.
+Next Obligation. apply Zcompare_antisym. Qed.
+Next Obligation.
+destruct c. unfold compare31 in *.
+rewrite Z.compare_eq_iff in *. congruence.
+eapply Zcompare_Lt_trans. apply H. apply H0.
+eapply Zcompare_Gt_trans. apply H. apply H0.
+Qed.
+Next Obligation.
+intros x y H. unfold compare, compare31 in H.
+rewrite Z.compare_eq_iff in *.
+rewrite <- surj_inj_compat, <- phi_inv_phi with (inj y), <- H.
+rewrite phi_inv_phi, surj_inj_compat; reflexivity.
+Qed.
+Next Obligation.
+rewrite iter_int31_iter_nat.
+pose proof (inj_bound_spec x).
+match goal with |- In x (fst ?p) => destruct p as [] eqn:? end.
+replace inj_bound with i in H.
+revert l i Heqp x H.
+induction (Z.abs_nat (phi inj_bound)); intros.
+inversion Heqp; clear Heqp; subst.
+rewrite spec_0 in H. pose proof (phi_bounded (inj x)). omega.
+simpl in Heqp.
+destruct nat_rect; specialize (IHn _ _ (eq_refl _) x); simpl in *.
+inversion Heqp. subst. clear Heqp.
+rewrite phi_incr in H.
+pose proof (phi_bounded i0).
+pose proof (phi_bounded (inj x)).
+destruct (Z_lt_le_dec (Z.succ (phi i0)) (2 ^ Z.of_nat size)%Z).
+rewrite Zmod_small in H by omega.
+apply Zlt_succ_le, Zle_lt_or_eq in H.
+destruct H; simpl; auto. left.
+rewrite <- surj_inj_compat, <- phi_inv_phi with (inj x), H, phi_inv_phi; reflexivity.
+replace (Z.succ (phi i0)) with (2 ^ Z.of_nat size)%Z in H by omega.
+rewrite Z_mod_same_full in H.
+exfalso; omega.
+rewrite <- phi_inv_phi with i, <- phi_inv_phi with inj_bound; f_equal.
+pose proof (phi_bounded inj_bound); pose proof (phi_bounded i).
+rewrite <- Z.abs_eq with (phi i), <- Z.abs_eq with (phi inj_bound) by omega.
+clear H H0 H1.
+do 2 rewrite <- Zabs2Nat.id_abs.
+f_equal.
+revert l i Heqp.
+assert (Z.abs_nat (phi inj_bound) < Z.abs_nat (2^31)).
+apply Zabs_nat_lt, phi_bounded.
+induction (Z.abs_nat (phi inj_bound)); intros.
+inversion Heqp; reflexivity.
+inversion Heqp; clear H1 H2 Heqp.
+match goal with |- _ (_ (_ (snd ?p))) = _ => destruct p end.
+pose proof (phi_bounded i0).
+erewrite <- IHn, <- Zabs2Nat.inj_succ in H |- *; eauto; try omega.
+rewrite phi_incr, Zmod_small; intuition; try omega.
+apply inj_lt in H.
+pose proof Z.le_le_succ_r.
+do 2 rewrite Zabs2Nat.id_abs, Z.abs_eq in H; now eauto.
+Qed.
+
+(** Previous class instances for [option A] **)
+Program Instance OptionComparable {A:Type} (C:Comparable A) : Comparable (option A) :=
+  { compare := fun x y =>
+      match x, y return comparison with
+        | None, None => Eq
+        | None, Some _ => Lt
+        | Some _, None => Gt
+        | Some x, Some y => compare x y
+      end }.
+Next Obligation.
+destruct x, y; intuition.
+apply compare_antisym.
+Qed.
+Next Obligation.
+destruct x, y, z; try now intuition;
+try (rewrite <- H in H0; discriminate).
+apply (compare_trans _ _ _ _ H H0).
+Qed.
+
+Instance OptionComparableUsualEq {A:Type} {C:Comparable A} (U:ComparableUsualEq C) :
+  ComparableUsualEq (OptionComparable C).
+Proof.
+intros x y.
+destruct x, y; intuition; try discriminate.
+rewrite (compare_eq a a0); intuition.
+Qed.
+
+Program Instance OptionFinite {A:Type} (E:Finite A) : Finite (option A) :=
+  { all_list := None :: map Some all_list }.
+Next Obligation.
+destruct x; intuition.
+right.
+apply in_map.
+apply all_list_forall.
+Defined.
+
+(** Definitions of [FSet]/[FMap] from [Comparable] **)
+Require Import OrderedTypeAlt.
+Require FSetAVL.
+Require FMapAVL.
+Import OrderedType.
+
+Module Type ComparableM.
+  Parameter t : Type.
+  Declare Instance tComparable : Comparable t.
+End ComparableM.
+
+Module OrderedTypeAlt_from_ComparableM (C:ComparableM) <: OrderedTypeAlt.
+  Definition t := C.t.
+  Definition compare : t -> t -> comparison := compare.
+
+  Infix "?=" := compare (at level 70, no associativity).
+
+  Lemma compare_sym x y : (y?=x) = CompOpp (x?=y).
+  Proof. exact (Logic.eq_sym (compare_antisym x y)). Qed.
+  Lemma compare_trans c x y z :
+    (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
+  Proof.
+  apply compare_trans.
+  Qed.
+End OrderedTypeAlt_from_ComparableM.
+
+Module OrderedType_from_ComparableM (C:ComparableM) <: OrderedType.
+  Module Alt := OrderedTypeAlt_from_ComparableM C.
+  Include (OrderedType_from_Alt Alt).
+End OrderedType_from_ComparableM.

src/Automaton.v

+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          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 General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+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. **)