diff options
| author | Pierre-Marie Pédrot | 2016-05-11 19:10:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-11 19:10:04 +0200 |
| commit | 4d9bcbda2fbf09939cddff4e4b42e5397d8a5cf1 (patch) | |
| tree | c41decbdd8bb9eb81c076cdea6d1c64bbcb0ff94 /parsing/entry.mli | |
| parent | 6be542f4ccb1d7fe95a65f4600f202a2424370d9 (diff) | |
| parent | 9acfdfd9b7d1cae34b97a4c06c52c4646e15589b (diff) | |
Thorough rewriting of the Pcoq API towards safety and static invariants.
Amongst other things:
1. No more unsafe grammar extensions, except when going through the CAMLPX-based
Pcoq.Gram module. This is mostly safe because CAMLPX adds casts to ensure that
parsing rules are well-typed. In particular, constr notation is now based on
GADTs ensuring well-typedness.
2. Less reliance on unsafe coq inside Pcoq, and exposing a self-contained API.
The Entry module was also removed as it now results useless.
3. Purely functional API for synchronized grammar extension. This gets rid of
quite buggy code maintaining a table of empty entries to work around CAMLPX bugs.
The state modification is now explicit and grammar extensions synchronized with
the summary must provide the rules they want to perform instead of doing so
imperatively.
Diffstat (limited to 'parsing/entry.mli')
| -rw-r--r-- | parsing/entry.mli | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/parsing/entry.mli b/parsing/entry.mli deleted file mode 100644 index 4c73fe2049..0000000000 --- a/parsing/entry.mli +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Typed grammar entries *) - -type 'a t -(** Typed grammar entries. We need to defined them here so that they are - marshallable and defined before the Pcoq.Gram module. They are basically - unique names. They should be kept synchronized with the {!Pcoq} entries. *) - -val create : string -> 'a t -(** Create an entry. They should be synchronized with the entries defined in - {!Pcoq}. *) - -(** {5 Meta-programming} *) - -val repr : 'a t -> string -val unsafe_of_name : string -> 'a t |