summaryrefslogtreecommitdiff
path: root/parsing/egrammar.ml
blob: 4418a45f7cce90dce6ec38895b9df453523e343f (plain)
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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Pp
open Compat
open Util
open Pcoq
open Extend
open Ppextend
open Topconstr
open Genarg
open Libnames
open Nameops
open Tacexpr
open Names
open Vernacexpr

(**************************************************************************)
(*
 * --- Note on the mapping of grammar productions to camlp4 actions ---
 *
 * Translation of environments: a production
 *   [ nt1(x1) ... nti(xi) ] -> act(x1..xi)
 * is written (with camlp4 conventions):
 *   (fun vi -> .... (fun v1 -> act(v1 .. vi) )..)
 * where v1..vi are the values generated by non-terminals nt1..nti.
 * Since the actions are executed by substituting an environment,
 * the make_*_action family build the following closure:
 *
 *      ((fun env ->
 *          (fun vi ->
 *             (fun env -> ...
 *
 *                  (fun v1 ->
 *                     (fun env -> gram_action .. env act)
 *                     ((x1,v1)::env))
 *                  ...)
 *             ((xi,vi)::env)))
 *         [])
 *)

(**********************************************************************)
(** Declare Notations grammar rules                                   *)

let constr_expr_of_name (loc,na) = match na with
  | Anonymous -> CHole (loc,None)
  | Name id -> CRef (Ident (loc,id))

let cases_pattern_expr_of_name (loc,na) = match na with
  | Anonymous -> CPatAtom (loc,None)
  | Name id -> CPatAtom (loc,Some (Ident (loc,id)))

type grammar_constr_prod_item =
  | GramConstrTerminal of Tok.t
  | GramConstrNonTerminal of constr_prod_entry_key * identifier option
  | GramConstrListMark of int * bool
    (* tells action rule to make a list of the n previous parsed items; 
       concat with last parsed list if true *)

let make_constr_action
  (f : loc -> constr_notation_substitution -> constr_expr) pil =
  let rec make (constrs,constrlists,binders as fullsubst) = function
  | [] ->
      Gram.action (fun loc -> f loc fullsubst)
  | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
      (* parse a non-binding item *)
      Gram.action (fun _ -> make fullsubst tl)
  | GramConstrNonTerminal (typ, Some _) :: tl ->
      (* parse a binding non-terminal *)
    (match typ with
    | (ETConstr _| ETOther _) ->
	Gram.action (fun (v:constr_expr) ->
	  make (v :: constrs, constrlists, binders) tl)
    | ETReference ->
        Gram.action (fun (v:reference) ->
	  make (CRef v :: constrs, constrlists, binders) tl)
    | ETName ->
        Gram.action (fun (na:name located) ->
	  make (constr_expr_of_name na :: constrs, constrlists, binders) tl)
    | ETBigint ->
        Gram.action (fun (v:Bigint.bigint) ->
	  make (CPrim(dummy_loc,Numeral v) :: constrs, constrlists, binders) tl)
    | ETConstrList (_,n) ->
	Gram.action (fun (v:constr_expr list) ->
	  make (constrs, v::constrlists, binders) tl)
    | ETBinder _ | ETBinderList (true,_) ->
	Gram.action (fun (v:local_binder list) ->
	  make (constrs, constrlists, v::binders) tl)
    | ETBinderList (false,_) ->
	Gram.action (fun (v:local_binder list list) ->
	  make (constrs, constrlists, List.flatten v::binders) tl)
    | ETPattern ->
	failwith "Unexpected entry of type cases pattern")
  | GramConstrListMark (n,b) :: tl ->
      (* Rebuild expansions of ConstrList *)
      let heads,constrs = list_chop n constrs in
      let constrlists =
	if b then (heads@List.hd constrlists)::List.tl constrlists
	else heads::constrlists
      in make (constrs, constrlists, binders) tl
  in
  make ([],[],[]) (List.rev pil)

let make_cases_pattern_action
  (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil =
  let rec make (env,envlist as fullenv) = function
  | [] ->
      Gram.action (fun loc -> f loc fullenv)
  | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
      (* parse a non-binding item *)
      Gram.action (fun _ -> make fullenv tl)
  | GramConstrNonTerminal (typ, Some _) :: tl ->
      (* parse a binding non-terminal *)
    (match typ with
    | ETConstr _ -> (* pattern non-terminal *)
        Gram.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl)
    | ETReference ->
        Gram.action (fun (v:reference) ->
	  make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl)
    | ETName ->
        Gram.action (fun (na:name located) ->
	  make (cases_pattern_expr_of_name na :: env, envlist) tl)
    | ETBigint ->
        Gram.action (fun (v:Bigint.bigint) ->
	  make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl)
    | ETConstrList (_,_) ->
        Gram.action  (fun (vl:cases_pattern_expr list) ->
	  make (env, vl :: envlist) tl)
    | (ETPattern | ETBinderList _ | ETBinder _ | ETOther _) ->
	failwith "Unexpected entry of type cases pattern or other")
  | GramConstrListMark (n,b) :: tl ->
      (* Rebuild expansions of ConstrList *)
      let heads,env = list_chop n env in
      if b then make (env,(heads@List.hd envlist)::List.tl envlist) tl
      else make (env,heads::envlist) tl
  in
  make ([],[]) (List.rev pil)

let rec make_constr_prod_item assoc from forpat = function
  | GramConstrTerminal tok :: l ->
      gram_token_of_token tok :: make_constr_prod_item assoc from forpat l
  | GramConstrNonTerminal (nt, ovar) :: l ->
      symbol_of_constr_prod_entry_key assoc from forpat nt
      :: make_constr_prod_item assoc from forpat l
  | GramConstrListMark _ :: l ->
      make_constr_prod_item assoc from forpat l
  | [] ->
      []

let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
  let entry =
    if forpat then weaken_entry Constr.pattern
    else weaken_entry Constr.operconstr in
  grammar_extend entry reinit (pos,[(name, p4assoc, [])])

let pure_sublevels level symbs =
  map_succeed
    (function s ->
       let i = level_of_snterml s in
       if level = Some i then failwith "";
       i)
    symbs

let extend_constr (entry,level) (n,assoc) mkact forpat rules =
  List.fold_left (fun nb pt ->
  let symbs = make_constr_prod_item assoc n forpat pt in
  let pure_sublevels = pure_sublevels level symbs in
  let needed_levels = register_empty_levels forpat pure_sublevels in
  let pos,p4assoc,name,reinit = find_position forpat assoc level in
  let nb_decls = List.length needed_levels + 1 in
  List.iter (prepare_empty_levels forpat) needed_levels;
  grammar_extend entry reinit (pos,[(name, p4assoc, [symbs, mkact pt])]);
  nb_decls) 0 rules

let extend_constr_notation (n,assoc,ntn,rules) =
  (* Add the notation in constr *)
  let mkact loc env = CNotation (loc,ntn,env) in
  let e = interp_constr_entry_key false (ETConstr (n,())) in
  let nb = extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rules in
  (* Add the notation in cases_pattern *)
  let mkact loc env = CPatNotation (loc,ntn,env) in
  let e = interp_constr_entry_key true (ETConstr (n,())) in
  let nb' = extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact)
    true rules in
  nb+nb'

(**********************************************************************)
(** Making generic actions in type generic_argument                   *)

let make_generic_action
  (f:loc -> ('b * raw_generic_argument) list -> 'a) pil =
  let rec make env = function
    | [] ->
	Gram.action (fun loc -> f loc env)
    | None :: tl -> (* parse a non-binding item *)
        Gram.action (fun _ -> make env tl)
    | Some (p, t) :: tl -> (* non-terminal *)
        Gram.action (fun v -> make ((p,in_generic t v) :: env) tl) in
  make [] (List.rev pil)

let make_rule univ f g pt =
  let (symbs,ntl) = List.split (List.map g pt) in
  let act = make_generic_action f ntl in
  (symbs, act)

(**********************************************************************)
(** Grammar extensions declared at ML level                           *)

type grammar_prod_item =
  | GramTerminal of string
  | GramNonTerminal of
      loc * argument_type * prod_entry_key * identifier option

let make_prod_item = function
  | GramTerminal s -> (gram_token_of_string s, None)
  | GramNonTerminal (_,t,e,po) ->
      (symbol_of_prod_entry_key e, Option.map (fun p -> (p,t)) po)

(* Tactic grammar extensions *)

let extend_tactic_grammar s gl =
  let univ = get_univ "tactic" in
  let mkact loc l = Tacexpr.TacExtend (loc,s,List.map snd l) in
  let rules = List.map (make_rule univ mkact make_prod_item) gl in
  maybe_uncurry (Gram.extend Tactic.simple_tactic)
    (None,[(None, None, List.rev rules)])

(* Vernac grammar extensions *)

let vernac_exts = ref []
let get_extend_vernac_grammars () = !vernac_exts

let extend_vernac_command_grammar s nt gl =
  let nt = Option.default Vernac_.command nt in
  vernac_exts := (s,gl) :: !vernac_exts;
  let univ = get_univ "vernac" in
  let mkact loc l = VernacExtend (s,List.map snd l) in
  let rules = List.map (make_rule univ mkact make_prod_item) gl in
  maybe_uncurry (Gram.extend nt) (None,[(None, None, List.rev rules)])

(**********************************************************************)
(** Grammar declaration for Tactic Notation (Coq level)               *)

let get_tactic_entry n =
  if n = 0 then
    weaken_entry Tactic.simple_tactic, None
  else if n = 5 then
    weaken_entry Tactic.binder_tactic, None
  else if 1<=n && n<5 then
    weaken_entry Tactic.tactic_expr, Some (Compat.Level (string_of_int n))
  else
    error ("Invalid Tactic Notation level: "^(string_of_int n)^".")

(* Declaration of the tactic grammar rule *)

let head_is_ident = function GramTerminal _::_ -> true | _ -> false

let add_tactic_entry (key,lev,prods,tac) =
  let univ = get_univ "tactic" in
  let entry, pos = get_tactic_entry lev in
  let rules =
    if lev = 0 then begin
      if not (head_is_ident prods) then
	error "Notation for simple tactic must start with an identifier.";
      let mkact s tac loc l =
	(TacAlias(loc,s,l,tac):raw_atomic_tactic_expr) in
      make_rule univ (mkact key tac) make_prod_item prods
    end
    else
      let mkact s tac loc l =
	(TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in
      make_rule univ (mkact key tac) make_prod_item prods in
  synchronize_level_positions ();
  grammar_extend entry None (pos,[(None, None, List.rev [rules])]);
  1

(**********************************************************************)
(** State of the grammar extensions                                   *)

type notation_grammar =
    int * gram_assoc option * notation * grammar_constr_prod_item list list

type all_grammar_command =
  | Notation of
	 (precedence * tolerability list) *
	  notation_var_internalization_type list *
	  notation_grammar
  | TacticGrammar of
      (string * int * grammar_prod_item list *
         (dir_path * Tacexpr.glob_tactic_expr))

let (grammar_state : (int * all_grammar_command) list ref) = ref []

let extend_grammar gram =
  let nb = match gram with
  | Notation (_,_,a) -> extend_constr_notation a
  | TacticGrammar g -> add_tactic_entry g in
  grammar_state := (nb,gram) :: !grammar_state

let recover_notation_grammar ntn prec =
  let l = map_succeed (function
    | _, Notation (prec',vars,(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' ->
	 vars, x
    | _ ->
	 failwith "") !grammar_state in
  assert (List.length l = 1);
  List.hd l

(* Summary functions: the state of the lexer is included in that of the parser.
   Because the grammar affects the set of keywords when adding or removing
   grammar rules. *)
type frozen_t = all_grammar_command list * Lexer.frozen_t

let freeze () = (!grammar_state, Lexer.freeze ())

(* We compare the current state of the grammar and the state to unfreeze,
   by computing the longest common suffixes *)
let factorize_grams l1 l2 =
  if l1 == l2 then ([], [], l1) else list_share_tails l1 l2

let number_of_entries gcl =
  List.fold_left (fun n (p,_) -> n + p) 0 gcl

let unfreeze (grams, lex) =
  let (undo, redo, common) = factorize_grams !grammar_state grams in
  let n = number_of_entries undo in
  remove_grammars n;
  remove_levels n;
  grammar_state := common;
  Lexer.unfreeze lex;
  List.iter extend_grammar (List.rev (List.map snd redo))

let init_grammar () =
  remove_grammars (number_of_entries !grammar_state);
  grammar_state := []

let init () =
  init_grammar ()

open Summary

let _ =
  declare_summary "GRAMMAR_LEXER"
    { freeze_function = freeze;
      unfreeze_function = unfreeze;
      init_function = init }