Source file `egramml.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Util
open Extend
open Pcoq
open Genarg
open Vernacexpr

(** Grammar extensions declared at ML level *)

type 's grammar_prod_item =
  | GramTerminal of string
  | GramNonTerminal :
      ('a raw_abstract_argument_type * ('s, _, 'a) Symbol.t) Loc.located -> 's grammar_prod_item

type 'a ty_arg = ('a -> raw_generic_argument)

type ('self, 'tr, _, 'r) ty_rule =
| TyStop : ('self, Gramlib.Grammar.norec, 'r, 'r) ty_rule
| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Symbol.t * 'b ty_arg option ->
  ('self, Gramlib.Grammar.mayrec, 'b -> 'a, 'r) ty_rule

type ('self, 'r) any_ty_rule =
| AnyTyRule : ('self, _, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule

let rec ty_rule_of_gram = function
| [] -> AnyTyRule TyStop
| GramTerminal s :: rem ->
  let AnyTyRule rem = ty_rule_of_gram rem in
  let tok = Pcoq.Symbol.token (Pcoq.terminal s) in
  let r = TyNext (rem, tok, None) in
  AnyTyRule r
| GramNonTerminal (_, (t, tok)) :: rem ->
  let AnyTyRule rem = ty_rule_of_gram rem in
  let inj = Some (fun obj -> Genarg.in_gen t obj) in
  let r = TyNext (rem, tok, inj) in
  AnyTyRule r

let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.Rule.t = function
| TyStop -> Pcoq.Rule.stop
| TyNext (rem, tok, _) -> Pcoq.Rule.next (ty_erase rem) tok

type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r

let rec ty_eval : type s tr a. (s, tr, a, Loc.t -> s) ty_rule -> s gen_eval -> a = function
| TyStop -> fun f loc -> f loc []
| TyNext (rem, tok, None) -> fun f _ -> ty_eval rem f
| TyNext (rem, tok, Some inj) -> fun f x ->
  let f loc args = f loc (inj x :: args) in
  ty_eval rem f

let make_rule f prod =
  let AnyTyRule ty_rule = ty_rule_of_gram (List.rev prod) in
  let symb = ty_erase ty_rule in
  let f loc l = f loc (List.rev l) in
  let act = ty_eval ty_rule f in
  Pcoq.Production.make symb act

let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function
| TUentry a -> ExtraArg a
| TUentryl (a,l) -> ExtraArg a
| TUopt(o) -> OptArg (proj_symbol o)
| TUlist1 l -> ListArg (proj_symbol l)
| TUlist1sep (l,_) -> ListArg (proj_symbol l)
| TUlist0 l -> ListArg (proj_symbol l)
| TUlist0sep (l,_) -> ListArg (proj_symbol l)

(** Vernac grammar extensions *)

let vernac_exts = Hashtbl.create 211

let get_extend_vernac_rule s =
  snd (Hashtbl.find vernac_exts s)

let declare_vernac_command_grammar ~allow_override s nt gl =
  let () = if not allow_override && Hashtbl.mem vernac_exts s
    then CErrors.anomaly Pp.(str "bad vernac extend: " ++ str s.ext_entry ++ str ", " ++ int s.ext_index)
  in
  let nt = Option.default Pvernac.Vernac_.command nt in
  Hashtbl.add vernac_exts s (nt, gl)

type any_extend_statement = Extend : 'a Entry.t * 'a extend_statement -> any_extend_statement

let extend_vernac_command_grammar s =
  let nt, gl = Hashtbl.find vernac_exts s in
  let mkact loc l = VernacSynterp (VernacExtend (s, l)) in
  let rules = [make_rule mkact gl] in
  if Pcoq.Entry.is_empty nt then
    (* Small hack to tolerate empty entries in VERNAC { ... } EXTEND *)
    Extend (nt, (Pcoq.Fresh (Gramlib.Gramext.First, [None, None, rules])))
  else
    Extend (nt, (Pcoq.Reuse (None, rules)))

let to_extend_rules (Extend (nt, r)) = [ExtendRule (nt,r)]

let extend_vernac = Pcoq.create_grammar_command "VernacExtend" {
    gext_fun = (fun s st -> to_extend_rules @@ extend_vernac_command_grammar s, st);
    gext_eq = (==); (* FIXME *)
  }

let extend_vernac_command_grammar ~undoable s =
  if undoable then Pcoq.extend_grammar_command extend_vernac s
  else
    let Extend (nt, r) = extend_vernac_command_grammar s in
    grammar_extend nt r

let grammar_exts = Hashtbl.create 21

let declare_grammar_ext ~uid e =
  let () = if Hashtbl.mem grammar_exts uid
    then CErrors.anomaly Pp.(str "bad grammar extend uid: " ++ str uid)
  in
  Hashtbl.add grammar_exts uid e

let extend_grammar = Pcoq.create_grammar_command "GrammarExtend" {
    gext_fun = (fun s st -> to_extend_rules @@ Hashtbl.find grammar_exts s, st);
    gext_eq = (==); (* FIXME *)
  }

let grammar_extend ?plugin_uid nt r = match plugin_uid with
  | None ->
    Pcoq.grammar_extend nt r
  | Some (plugin,uid) ->
    let uid = plugin^":"^uid in
    declare_grammar_ext ~uid (Extend (nt, r));
    Mltop.add_init_function plugin (fun () ->
        Pcoq.extend_grammar_command extend_grammar uid)