aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/MenhirLib/Tuples.v
diff options
context:
space:
mode:
authorJacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>2019-07-05 15:15:42 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2019-07-05 15:15:42 +0200
commit998f3c5ff90f6230b722b6094761f5989beea0a5 (patch)
treead107d40768bf6e40ba7d8493b2fa6f01c668231 /cparser/MenhirLib/Tuples.v
parentda929bc61ccd67d2be2b1e5d3cd9f3cb60f56074 (diff)
downloadcompcert-998f3c5ff90f6230b722b6094761f5989beea0a5.tar.gz
compcert-998f3c5ff90f6230b722b6094761f5989beea0a5.zip
New parser based on new version of the Coq backend of Menhir (#276)
What's new: 1. A rewrite of the Coq interpreter of Menhir automaton, with dependent types removing the need for runtime checks for the well-formedness of the LR stack. This seem to cause some speedup on the parsing time (~10% for lexing + parsing). 2. Thanks to 1., it is now possible to avoid the use of int31 for comparing symbols: Since this is only used for validation, positives are enough. 3. Speedup of Validation: on my machine, the time needed for compiling Parser.v goes from about 2 minutes to about 1 minute. This seem to be related to a performance bug in the completeness validator and to the use of positive instead of int31. 3. Menhir now generates a dedicated inductive type for (semantic-value-carrying) tokens (in addition to the already existing inductive type for (non-semantic-value-carrying) terminals. The end result is that the OCaml support code for the parser no longer contain calls to Obj.magic. The bad side of this change is that the formal specification of the parser is perhaps harder to read. 4. The parser and its library are now free of axioms (I used to use axiom K and proof irrelevance for easing proofs involving dependent types). 5. Use of a dedicated custom negative coinductive type for the input stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a positive coinductive type, which are now deprecated by Coq. 6. The fuel of the parser is now specified using its logarithm instead of its actual value. This makes it possible to give large fuel values instead of using the `let rec fuel = S fuel` hack. 7. Some refactoring in the lexer, the parser and the Cabs syntax tree. The corresponding changes in Menhir have been released as part of version 20190626. The `MenhirLib` directory is identical to the content of the `src` directory of the corresponding `coq-menhirlib` opam package except that: - In order to try to make CompCert compatible with several Menhir versions without updates, we do not check the version of menhir is compatible with the version of coq-menhirlib. Hence the `Version.v` file is not present in CompCert's copy. - Build-system related files have been removed.
Diffstat (limited to 'cparser/MenhirLib/Tuples.v')
-rw-r--r--cparser/MenhirLib/Tuples.v49
1 files changed, 0 insertions, 49 deletions
diff --git a/cparser/MenhirLib/Tuples.v b/cparser/MenhirLib/Tuples.v
deleted file mode 100644
index 3fd2ec03..00000000
--- a/cparser/MenhirLib/Tuples.v
+++ /dev/null
@@ -1,49 +0,0 @@
-(* *********************************************************************)
-(* *)
-(* 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. *)
-(* *)
-(* *********************************************************************)
-
-Require Import List.
-Require Import Coq.Program.Syntax.
-Require Import Equality.
-
-(** A curryfied function with multiple parameters **)
-Definition arrows_left: list Type -> Type -> Type :=
- fold_left (fun A B => B -> A).
-
-(** A curryfied function with multiple parameters **)
-Definition arrows_right: Type -> list Type -> Type :=
- fold_right (fun A B => A -> B).
-
-(** A tuple is a heterogeneous list. For convenience, we use pairs. **)
-Fixpoint tuple (types : list Type) : Type :=
- match types with
- | nil => unit
- | t::q => prod t (tuple q)
- end.
-
-Fixpoint uncurry {args:list Type} {res:Type}:
- arrows_left args res -> tuple args -> res :=
- match args return forall res, arrows_left args res -> tuple args -> res with
- | [] => fun _ f _ => f
- | t::q => fun res f p => let (d, t) := p in
- (@uncurry q _ f t) d
- end res.
-
-Lemma JMeq_eqrect:
- forall (U:Type) (a b:U) (P:U -> Type) (x:P a) (e:a=b),
- eq_rect a P x b e ~= x.
-Proof.
-destruct e.
-reflexivity.
-Qed.