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

6 files changed, 83 insertions, 81 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index d866882dbd..89b9e6de30 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-10-30-V1"
+  CACHEKEY: "bionic_coq-V2018-11-07-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 6201bc9610..576a648b48 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.03)
+   - Camlp5 (version >= 7.06)
      (available at https://camlp5.github.io/)
 
    - GNU Make version 3.81 or later
diff --git a/configure.ml b/configure.ml
index 39c65683ff..14c1f38a95 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 > 6 || (s2i major, s2i minor) >= (6,6) ->
+  | major::minor::_ when s2i major > 7 || (s2i major, s2i minor) >= (7,6) ->
     cprintf "You have Camlp5 %s. Good!" version; version
-  | _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n"
+  | _ -> die "Error: unsupported Camlp5 (version < 7.06 or unrecognized).\n"
 
 let config_camlp5 () =
     let camlp5mod = "gramlib" in
diff --git a/coq.opam b/coq.opam
index ab18119ac4..cfcb310d10 100644
--- a/coq.opam
+++ b/coq.opam
@@ -22,7 +22,7 @@ depends: [
   "ocaml"     {         >= "4.05.0" }
   "dune"      { build & >= "1.4.0"  }
   "num"
-  "camlp5"    {         >= "7.03"   }
+  "camlp5"    {         >= "7.06"   }
 ]
 
 build-env: [
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 4ddb582414..0439d566fd 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-10-30-V1"
+# CACHEKEY: "bionic_coq-V2018-11-07-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.03" \
+ENV CAMLP5_VER="7.06" \
     COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
 
 # base switch
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index eb3e633892..fbdadbc0f2 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -83,13 +83,9 @@ 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
 
@@ -100,9 +96,6 @@ 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
 
@@ -113,7 +106,6 @@ 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) =
@@ -166,16 +158,9 @@ let of_coq_position = function
 | Extend.Level s -> Gramext.Level s
 
 module Symbols : sig
-  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
+  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
 end = struct
 
   let stoken tok =
@@ -190,19 +175,10 @@ end = struct
     | Tok.BULLET s -> "BULLET", s
     | Tok.EOI -> "EOI", ""
     in
-    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
+    G.s_token pattern
 
+  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 =
@@ -224,40 +200,41 @@ let camlp5_verbosity silent f x =
 
 (** Binding general entry keys to symbol *)
 
-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
+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
 | Rules (r, act) ->
-  let symb = symbol_of_rule r.norec_rule [] in
-  let act = of_coq_action r.norec_rule act in
-  (symb, 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 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_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_single_extend_statement (lvl, assoc, rule) =
   (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule)
@@ -265,6 +242,13 @@ 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
 
@@ -291,6 +275,22 @@ 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,13 +309,15 @@ let 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 redo () = camlp5_verbosity false (uncurry (G.extend e)) ext in
+  let ext = fix_extend_statement ext in
+  let redo () = camlp5_verbosity false (uncurry (G.safe_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;
-  camlp5_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext)
+  let ext = fix_extend_statement (of_coq_extend_statement ext) in
+  camlp5_verbosity false (uncurry (G.safe_extend e)) ext
 
 (** The apparent parser of Coq; encapsulate G to keep track
     of the extensions. *)
@@ -327,7 +329,7 @@ module Gram =
       curry
     (fun ext ->
       camlp5_state :=
-        (ByEXTEND ((fun () -> grammar_delete e None ext),
+        (ByEXTEND ((fun () -> unsafe_grammar_delete e None ext),
            (fun () -> uncurry (G.extend e) ext)))
       :: !camlp5_state;
       uncurry (G.extend e) ext)
@@ -380,16 +382,16 @@ let make_rule r = [None, None, r]
 
 let eoi_entry en =
   let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in
-  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]);
+  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)]);
   e
 
 let map_entry f en =
   let e = Entry.create ((Gram.Entry.name en) ^ "_map") in
-  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]);
+  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)]);
   e
 
 (* Parse a string, does NOT check if the entire string was read
@@ -516,10 +518,10 @@ module Module =
   end
 
 let epsilon_value f e =
-  let r = Rule (Next (Stop, e), fun x _ -> f x) in
-  let ext = of_coq_extend_statement (None, [None, None, [r]]) in
+  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 entry = Gram.entry_create "epsilon" in
-  let () = uncurry (G.extend entry) ext in
+  let () = G.safe_extend entry None ext in
   try Some (parse_string entry "") with _ -> None
 
 (** Synchronized grammar extensions *)