Revert "Merge PR #8923: Bump camlp5 minimal version and use its safe API."

This reverts commit c4880effb91fab55c250a799cbceac9b04681db0, reversing
changes made to 65927c22bcad62e1bc9a28a57377d82eba215a2d.

6 files changed, 81 insertions, 83 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 89b9e6de30..d866882dbd 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -9,7 +9,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2018-11-07-V1"
+  CACHEKEY: "bionic_coq-V2018-10-30-V1"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
diff --git a/INSTALL b/INSTALL
index 576a648b48..6201bc9610 100644
--- a/INSTALL
+++ b/INSTALL
@@ -39,7 +39,7 @@ WHAT DO YOU NEED ?
    - Findlib (version >= 1.4.1)
      (available at http://projects.camlcity.org/projects/findlib.html)
 
-   - Camlp5 (version >= 7.06)
+   - Camlp5 (version >= 7.03)
      (available at https://camlp5.github.io/)
 
    - GNU Make version 3.81 or later
diff --git a/configure.ml b/configure.ml
index 14c1f38a95..39c65683ff 100644
--- a/configure.ml
+++ b/configure.ml
@@ -709,9 +709,9 @@ let check_camlp5_version camlp5o =
   let version_line, _ = run ~err:StdOut camlp5o ["-v"] in
   let version = List.nth (string_split ' ' version_line) 2 in
   match numeric_prefix_list version with
-  | major::minor::_ when s2i major > 7 || (s2i major, s2i minor) >= (7,6) ->
+  | major::minor::_ when s2i major > 6 || (s2i major, s2i minor) >= (6,6) ->
     cprintf "You have Camlp5 %s. Good!" version; version
-  | _ -> die "Error: unsupported Camlp5 (version < 7.06 or unrecognized).\n"
+  | _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n"
 
 let config_camlp5 () =
     let camlp5mod = "gramlib" in
diff --git a/coq.opam b/coq.opam
index cfcb310d10..ab18119ac4 100644
--- a/coq.opam
+++ b/coq.opam
@@ -22,7 +22,7 @@ depends: [
   "ocaml"     {         >= "4.05.0" }
   "dune"      { build & >= "1.4.0"  }
   "num"
-  "camlp5"    {         >= "7.06"   }
+  "camlp5"    {         >= "7.03"   }
 ]
 
 build-env: [
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 0439d566fd..4ddb582414 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-11-07-V1"
+# CACHEKEY: "bionic_coq-V2018-10-30-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -41,7 +41,7 @@ ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.4.0 ounit.2.0.8 odoc.1.3.0" \
     CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
-ENV CAMLP5_VER="7.06" \
+ENV CAMLP5_VER="7.03" \
     COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
 
 # base switch
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index fbdadbc0f2..eb3e633892 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -83,9 +83,13 @@ module type S =
   *)
 
   type 'a entry = 'a Entry.e
+  type internal_entry = Tok.t Gramext.g_entry
+  type symbol = Tok.t Gramext.g_symbol
+  type action = Gramext.g_action
   type coq_parsable
 
   val coq_parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
+  val action : 'a -> action
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> coq_parsable -> 'a
 
@@ -96,6 +100,9 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
   include Grammar.GMake(CLexer)
 
   type 'a entry = 'a Entry.e
+  type internal_entry = Tok.t Gramext.g_entry
+  type symbol = Tok.t Gramext.g_symbol
+  type action = Gramext.g_action
 
   type coq_parsable = parsable * CLexer.lexer_state ref
 
@@ -106,6 +113,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
     state := CLexer.get_lexer_state ();
     (a,state)
 
+  let action = Gramext.action
   let entry_create = Entry.create
 
   let entry_parse e (p,state) =
@@ -158,9 +166,16 @@ let of_coq_position = function
 | Extend.Level s -> Gramext.Level s
 
 module Symbols : sig
-  val stoken : Tok.t -> ('s, string) G.ty_symbol
-  val slist0sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol
-  val slist1sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol
+  val stoken : Tok.t -> G.symbol
+  val sself : G.symbol
+  val snext : G.symbol
+  val slist0 : G.symbol -> G.symbol
+  val slist0sep : G.symbol * G.symbol -> G.symbol
+  val slist1 : G.symbol -> G.symbol
+  val slist1sep : G.symbol * G.symbol -> G.symbol
+  val sopt : G.symbol -> G.symbol
+  val snterml : G.internal_entry * string -> G.symbol
+  val snterm : G.internal_entry -> G.symbol
 end = struct
 
   let stoken tok =
@@ -175,10 +190,19 @@ end = struct
     | Tok.BULLET s -> "BULLET", s
     | Tok.EOI -> "EOI", ""
     in
-    G.s_token pattern
+    Gramext.Stoken pattern
+
+     let slist0sep (x, y) = Gramext.Slist0sep (x, y, false)
+     let slist1sep (x, y) = Gramext.Slist1sep (x, y, false)
+
+  let snterml (x, y) = Gramext.Snterml (x, y)
+  let snterm x = Gramext.Snterm x
+  let sself = Gramext.Sself
+  let snext = Gramext.Snext
+  let slist0 x = Gramext.Slist0 x
+  let slist1 x = Gramext.Slist1 x
+  let sopt x = Gramext.Sopt x
 
-  let slist0sep x y = G.s_list0sep x y false
-  let slist1sep x y = G.s_list1sep x y false
 end
 
 let camlp5_verbosity silent f x =
@@ -200,41 +224,40 @@ let camlp5_verbosity silent f x =
 
 (** Binding general entry keys to symbol *)
 
-type ('s, 'a, 'r) casted_rule = Casted : ('s, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, 'a, 'r) casted_rule
-
-let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> (s, a) G.ty_symbol = function
-| Atoken t -> Symbols.stoken t
-| Alist1 s -> G.s_list1 (symbol_of_prod_entry_key s)
-| Alist1sep (s,sep) ->
-    Symbols.slist1sep (symbol_of_prod_entry_key s) (symbol_of_prod_entry_key sep)
-| Alist0 s -> G.s_list0 (symbol_of_prod_entry_key s)
-| Alist0sep (s,sep) ->
-    Symbols.slist0sep (symbol_of_prod_entry_key s) (symbol_of_prod_entry_key sep)
-| Aopt s -> G.s_opt (symbol_of_prod_entry_key s)
-| Aself -> G.s_self
-| Anext -> G.s_next
-| Aentry e -> G.s_nterm e
-| Aentryl (e, n) -> G.s_nterml e n
-| Arules rs -> G.s_rules (List.map symbol_of_rules rs)
-
-and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Ploc.t -> r) casted_rule = function
-| Stop -> Casted (G.r_stop, fun act loc -> act (!@loc))
-| Next (r, s) ->
-  let Casted (r, cast) = symbol_of_rule r in
-  Casted (G.r_next r (symbol_of_prod_entry_key s), (fun act x -> cast (act x)))
-
-and symbol_of_rules : type a. a Extend.rules -> a G.ty_production = function
+let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> G.action = function
+| Stop -> fun f -> G.action (fun loc -> f (!@ loc))
+| Next (r, _) -> fun f -> G.action (fun x -> of_coq_action r (f x))
+
+let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
+  | Atoken t -> Symbols.stoken t
+  | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s)
+  | Alist1sep (s,sep) ->
+      Symbols.slist1sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep)
+  | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s)
+  | Alist0sep (s,sep) ->
+      Symbols.slist0sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep)
+  | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s)
+  | Aself -> Symbols.sself
+  | Anext -> Symbols.snext
+  | Aentry e ->
+    Symbols.snterm (G.Entry.obj e)
+  | Aentryl (e, n) ->
+    Symbols.snterml (G.Entry.obj e, n)
+  | Arules rs ->
+    Gramext.srules (List.map symbol_of_rules rs)
+
+and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function
+| Stop -> fun accu -> accu
+| Next (r, s) -> fun accu -> symbol_of_rule r (symbol_of_prod_entry_key s :: accu)
+
+and symbol_of_rules : type a. a Extend.rules -> _ = function
 | Rules (r, act) ->
-  let Casted (symb, cast) = symbol_of_rule r.norec_rule in
-  G.production (symb, cast act)
-
-(** FIXME: This is a hack around a deficient camlp5 API *)
-type 'a any_production = AnyProduction : ('a, 'f, Ploc.t -> 'a) G.ty_rule * 'f -> 'a any_production
+  let symb = symbol_of_rule r.norec_rule [] in
+  let act = of_coq_action r.norec_rule act in
+  (symb, act)
 
-let of_coq_production_rule : type a. a Extend.production_rule -> a any_production = function
-| Rule (toks, act) ->
-  let Casted (symb, cast) = symbol_of_rule toks in
-  AnyProduction (symb, cast act)
+let of_coq_production_rule : type a. a Extend.production_rule -> _ = function
+| Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act)
 
 let of_coq_single_extend_statement (lvl, assoc, rule) =
   (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule)
@@ -242,13 +265,6 @@ let of_coq_single_extend_statement (lvl, assoc, rule) =
 let of_coq_extend_statement (pos, st) =
   (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st)
 
-let fix_extend_statement (pos, st) =
-  let fix_single_extend_statement (lvl, assoc, rules) =
-    let fix_production_rule (AnyProduction (s, act)) = G.production (s, act) in
-    (lvl, assoc, List.map fix_production_rule rules)
-  in
-  (pos, List.map fix_single_extend_statement st)
-
 (** Type of reinitialization data *)
 type gram_reinit = gram_assoc * gram_position
 
@@ -275,22 +291,6 @@ let camlp5_entries = ref EntryDataMap.empty
 let grammar_delete e reinit (pos,rls) =
   List.iter
     (fun (n,ass,lev) ->
-      List.iter (fun (AnyProduction (pil,_)) -> G.safe_delete_rule e pil) (List.rev lev))
-    (List.rev rls);
-  match reinit with
-  | Some (a,ext) ->
-    let a = of_coq_assoc a in
-    let ext = of_coq_position ext in
-    let lev = match pos with
-    | Some (Gramext.Level n) -> n
-    | _ -> assert false
-    in
-    (G.safe_extend e) (Some ext) [Some lev,Some a,[]]
-  | None -> ()
-
-let unsafe_grammar_delete e reinit (pos,rls) =
-  List.iter
-    (fun (n,ass,lev) ->
       List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev))
     (List.rev rls);
   match reinit with
@@ -309,15 +309,13 @@ let unsafe_grammar_delete e reinit (pos,rls) =
 let grammar_extend e reinit ext =
   let ext = of_coq_extend_statement ext in
   let undo () = grammar_delete e reinit ext in
-  let ext = fix_extend_statement ext in
-  let redo () = camlp5_verbosity false (uncurry (G.safe_extend e)) ext in
+  let redo () = camlp5_verbosity false (uncurry (G.extend e)) ext in
   camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state;
   redo ()
 
 let grammar_extend_sync e reinit ext =
   camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state;
-  let ext = fix_extend_statement (of_coq_extend_statement ext) in
-  camlp5_verbosity false (uncurry (G.safe_extend e)) ext
+  camlp5_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext)
 
 (** The apparent parser of Coq; encapsulate G to keep track
     of the extensions. *)
@@ -329,7 +327,7 @@ module Gram =
       curry
     (fun ext ->
       camlp5_state :=
-        (ByEXTEND ((fun () -> unsafe_grammar_delete e None ext),
+        (ByEXTEND ((fun () -> grammar_delete e None ext),
            (fun () -> uncurry (G.extend e) ext)))
       :: !camlp5_state;
       uncurry (G.extend e) ext)
@@ -382,16 +380,16 @@ let make_rule r = [None, None, r]
 
 let eoi_entry en =
   let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in
-  let symbs = G.r_next (G.r_next G.r_stop (G.s_nterm en)) (Symbols.stoken Tok.EOI) in
-  let act = fun _ x loc -> x in
-  Gram.safe_extend e None (make_rule [G.production (symbs, act)]);
+  let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in
+  let act = Gram.action (fun _ x loc -> x) in
+  uncurry (Gram.extend e) (None, make_rule [symbs, act]);
   e
 
 let map_entry f en =
   let e = Entry.create ((Gram.Entry.name en) ^ "_map") in
-  let symbs = G.r_next G.r_stop (G.s_nterm en) in
-  let act = fun x loc -> f x in
-  Gram.safe_extend e None (make_rule [G.production (symbs, act)]);
+  let symbs = [Symbols.snterm (Gram.Entry.obj en)] in
+  let act = Gram.action (fun x loc -> f x) in
+  uncurry (Gram.extend e) (None, make_rule [symbs, act]);
   e
 
 (* Parse a string, does NOT check if the entire string was read
@@ -518,10 +516,10 @@ module Module =
   end
 
 let epsilon_value f e =
-  let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in
-  let ext = [None, None, [r]] in
+  let r = Rule (Next (Stop, e), fun x _ -> f x) in
+  let ext = of_coq_extend_statement (None, [None, None, [r]]) in
   let entry = Gram.entry_create "epsilon" in
-  let () = G.safe_extend entry None ext in
+  let () = uncurry (G.extend entry) ext in
   try Some (parse_string entry "") with _ -> None
 
 (** Synchronized grammar extensions *)