diff options
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rw-r--r-- | INSTALL | 2 | ||||
| -rw-r--r-- | configure.ml | 4 | ||||
| -rw-r--r-- | coq.opam | 2 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 4 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 150 |
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" @@ -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 @@ -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 *) |