New parser based on new version of the Coq backend of Menhir

LICENSE

@@ -1,6 +1,6 @@
 All files in this distribution are part of the CompCert verified compiler.
 
-The CompCert verified compiler is Copyright by Institut National de 
+The CompCert verified compiler is Copyright by Institut National de
 Recherche en Informatique et en Automatique (INRIA) and
 AbsInt Angewandte Informatik GmbH.
 
@@ -9,12 +9,12 @@ INRIA Non-Commercial License Agreement given below or under the terms
 of a Software Usage Agreement of AbsInt Angewandte Informatik GmbH.
 The latter is a separate contract document.
 
-The INRIA Non-Commercial License Agreement is a non-free license that 
-grants you the right to use the CompCert verified compiler for 
-educational, research or evaluation purposes only, but prohibits 
+The INRIA Non-Commercial License Agreement is a non-free license that
+grants you the right to use the CompCert verified compiler for
+educational, research or evaluation purposes only, but prohibits
 any commercial use.
 
-For commercial use you need a Software Usage Agreement from 
+For commercial use you need a Software Usage Agreement from
 AbsInt Angewandte Informatik GmbH.
 
 The following files in this distribution are dual-licensed both under
@@ -38,15 +38,15 @@ option) any later version:
   cfrontend/Ctyping.v
   cfrontend/PrintClight.ml
   cfrontend/PrintCsyntax.ml
-  
+
   backend/Cminor.v
   backend/PrintCminor.ml
 
   all files in the cparser/ directory
 
   all files in the exportclight/ directory
 
-  the Archi.v, CBuiltins.ml, and extractionMachdep.v files 
+  the Archi.v, CBuiltins.ml, and extractionMachdep.v files
   in directories arm, powerpc, riscV, x86, x86_32, x86_64
 
   extraction/extraction.v
@@ -64,11 +64,14 @@ non-commercial contexts, subject to the terms of the GNU General
 Public License.
 
 The files contained in the flocq/ directory and its subdirectories are
-taken from the Flocq project, http://flocq.gforge.inria.fr/
-These files are Copyright 2010-2017 INRIA and distributed under the
-terms of the GNU Lesser General Public Licence, either version 3 of
-the licence, or (at your option) any later version.  A copy of the GNU
-Lesser General Public Licence version 3 is included below.
+taken from the Flocq project, http://flocq.gforge.inria.fr/. The files
+contained in the MenhirLib directory are taken from the Menhir
+project, http://gallium.inria.fr/~fpottier/menhir/. The files from the
+Flocq project and the files in the MenhirLib directory are Copyright
+2010-2019 INRIA and distributed under the terms of the GNU Lesser
+General Public Licence, either version 3 of the licence, or (at your
+option) any later version. A copy of the GNU Lesser General Public
+Licence version 3 is included below.
 
 The files contained in the runtime/ directory and its subdirectories
 are Copyright 2013-2017 INRIA and distributed under the terms of the BSD

Makefile

@@ -23,9 +23,10 @@ endif
 
 DIRS=lib common $(ARCHDIRS) backend cfrontend driver \
   flocq/Core flocq/Prop flocq/Calc flocq/IEEE754 \
-  exportclight cparser cparser/MenhirLib
+  exportclight MenhirLib cparser
 
-RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight cparser
+RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight \
+  MenhirLib cparser
 
 COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) compcert.$(d))
 
@@ -103,24 +104,24 @@ CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Ctyping.v Cstrategy.v Cexec.v \
   Cshmgen.v Cshmgenproof.v \
   Csharpminor.v Cminorgen.v Cminorgenproof.v
 
-# LR(1) parser validator
-
-PARSERVALIDATOR=Alphabet.v Interpreter_complete.v Interpreter.v \
-  Validator_complete.v Automaton.v Interpreter_correct.v Main.v \
-  Validator_safe.v Grammar.v Interpreter_safe.v Tuples.v
-
 # Parser
 
 PARSER=Cabs.v Parser.v
 
+# MenhirLib
+
+MENHIRLIB=Alphabet.v Automaton.v Grammar.v Interpreter_complete.v \
+  Interpreter_correct.v Interpreter.v Main.v Validator_complete.v \
+  Validator_safe.v Validator_classes.v
+
 # Putting everything together (in driver/)
 
 DRIVER=Compopts.v Compiler.v Complements.v
 
 # All source files
 
 FILES=$(VLIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \
-  $(PARSERVALIDATOR) $(PARSER)
+  $(MENHIRLIB) $(PARSER)
 
 # Generated source files
 
@@ -141,7 +142,6 @@ ifeq ($(CLIGHTGEN),true)
 	$(MAKE) clightgen
 endif
 
-
 proof: $(FILES:.v=.vo)
 
 # Turn off some warnings for compiling Flocq
@@ -225,7 +225,7 @@ driver/Version.ml: VERSION
 
 cparser/Parser.v: cparser/Parser.vy
 	@rm -f $@
-	$(MENHIR) $(MENHIR_FLAGS) --coq cparser/Parser.vy
+	$(MENHIR) --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check cparser/Parser.vy
 	@chmod a-w $@
 
 depend: $(GENERATED) depend1

Makefile.extr

@@ -50,8 +50,8 @@ INCLUDES=$(patsubst %,-I %, $(DIRS))
 # Control of warnings:
 
 WARNINGS=-w +a-4-9-27 -strict-sequence -safe-string -warn-error +a #Deprication returns with ocaml 4.03
-extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45
-extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45
+extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45-60
+extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45-60
 cparser/pre_parser.cmx: WARNINGS += -w -41
 cparser/pre_parser.cmo: WARNINGS += -w -41
 

MenhirLib/Alphabet.v

@@ -0,0 +1,247 @@
+(****************************************************************************)
+(*                                                                          *)
+(*                                   Menhir                                 *)
+(*                                                                          *)
+(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
+(*                                                                          *)
+(*  Copyright Inria. 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, as described in the file LICENSE.            *)
+(*                                                                          *)
+(****************************************************************************)
+
+From Coq Require Import 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 Leibniz equality. **)
+Class ComparableLeibnizEq {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:ComparableLeibnizEq 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.
+
+Instance NComparableLeibnizEq : ComparableLeibnizEq natComparable := Nat.compare_eq.
+
+(** A pair of ComparableLeibnizEq is ComparableLeibnizEq **)
+Instance PairComparableLeibnizEq
+  {A:Type} {CA:Comparable A} (UA:ComparableLeibnizEq CA)
+  {B:Type} {CB:Comparable B} (UB:ComparableLeibnizEq CB) :
+    ComparableLeibnizEq (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 [ComparableLeibnizEq] and [Finite]. **)
+Class Alphabet (A:Type) := {
+  AlphabetComparable :> Comparable A;
+  AlphabetComparableLeibnizEq :> ComparableLeibnizEq 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
+   [positive] **)
+Class Numbered (A:Type) := {
+  inj : A -> positive;
+  surj : positive -> A;
+  surj_inj_compat : forall x, surj (inj x) = x;
+  inj_bound : positive;
+  inj_bound_spec : forall x, (inj x < Pos.succ inj_bound)%positive
+}.
+
+Program Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A :=
+  { AlphabetComparable := {| compare := fun x y => Pos.compare (inj x) (inj y) |};
+    AlphabetFinite :=
+      {| all_list := fst (Pos.iter
+                           (fun '(l, p) => (surj p::l, Pos.succ p))
+                           ([], 1%positive) inj_bound) |} }.
+Next Obligation. simpl. now rewrite <- Pos.compare_antisym. Qed.
+Next Obligation.
+  match goal with c : comparison |- _ => destruct c end.
+  - rewrite Pos.compare_eq_iff in *. congruence.
+  - rewrite Pos.compare_lt_iff in *. eauto using Pos.lt_trans.
+  - rewrite Pos.compare_gt_iff in *. eauto using Pos.lt_trans.
+Qed.
+Next Obligation.
+  intros x y. unfold compare. intros Hxy.
+  assert (Hxy' : inj x = inj y).
+  (* We do not use [Pos.compare_eq_iff] directly to make sure the
+     proof is executable. *)
+  { destruct (Pos.eq_dec (inj x) (inj y)) as [|[]]; [now auto|].
+    now apply Pos.compare_eq_iff. }
+  (* Using rewrite here leads to non-executable proofs. *)
+  transitivity (surj (inj x)).
+  { apply eq_sym, surj_inj_compat. }
+  transitivity (surj (inj y)); cycle 1.
+  { apply surj_inj_compat. }
+  apply f_equal, Hxy'.
+Defined.
+Next Obligation.
+  rewrite <-(surj_inj_compat x).
+  generalize (inj_bound_spec x). generalize (inj x). clear x. intros x.
+  match goal with |- ?Hx -> In ?s (fst ?p) =>
+    assert ((Hx -> In s (fst p)) /\ snd p = Pos.succ inj_bound); [|now intuition] end.
+  rewrite Pos.lt_succ_r.
+  induction inj_bound as [|y [IH1 IH2]] using Pos.peano_ind;
+    (split; [intros Hx|]); simpl.
+  - rewrite (Pos.le_antisym _ _ Hx); auto using Pos.le_1_l.
+  - auto.
+  - rewrite Pos.iter_succ. destruct Pos.iter; simpl in *. subst.
+    rewrite Pos.le_lteq in Hx. destruct Hx as [?%Pos.lt_succ_r| ->]; now auto.
+  - rewrite Pos.iter_succ. destruct Pos.iter. simpl in IH2. subst. reflexivity.
+Qed.
+
+(** 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.