aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/egrammar.ml
blob: 74b275fabf75bad40b19a094d31b80487fe05afc (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
352
353
354
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id$ *)

open Pp
open Util
open Pcoq
open Extend
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                                   *)

type prod_item =
  | Term of Token.pattern
  | NonTerm of constr_production_entry * 
      (Names.identifier * constr_production_entry) option

type 'a action_env = (identifier * 'a) list

let make_constr_action
  (f : loc -> constr_expr action_env -> constr_expr) pil =
  let rec make (env : constr_expr action_env) = function
    | [] ->
	Gramext.action (fun loc -> f loc env)
    | None :: tl -> (* parse a non-binding item *)
        Gramext.action (fun _ -> make env tl)
    | Some (p, (ETConstr _| ETOther _)) :: tl -> (* constr non-terminal *)
        Gramext.action (fun (v:constr_expr) -> make ((p,v) :: env) tl)
    | Some (p, ETReference) :: tl -> (* non-terminal *)
        Gramext.action (fun (v:reference) -> make ((p,CRef v) :: env) tl)
    | Some (p, ETIdent) :: tl -> (* non-terminal *)
        Gramext.action (fun (v:identifier) ->
	  make ((p,CRef (Ident (dummy_loc,v))) :: env) tl)
    | Some (p, ETBigint) :: tl -> (* non-terminal *)
        Gramext.action (fun (v:Bigint.bigint) ->
	  make ((p,CPrim (dummy_loc,Numeral v)) :: env) tl)
    | Some (p, ETConstrList _) :: tl ->
        Gramext.action (fun (v:constr_expr list) ->
          let dummyid = Ident (dummy_loc,id_of_string "_") in
	  make ((p,CAppExpl (dummy_loc,(None,dummyid),v)) :: env) tl)
    | Some (p, ETPattern) :: tl -> 
	failwith "Unexpected entry of type cases pattern" in
  make [] (List.rev pil)

let make_cases_pattern_action
  (f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil =
  let rec make (env : cases_pattern_expr action_env) = function
    | [] ->
	Gramext.action (fun loc -> f loc env)
    | None :: tl -> (* parse a non-binding item *)
        Gramext.action (fun _ -> make env tl)
    | Some (p, ETConstr _) :: tl -> (* pattern non-terminal *)
        Gramext.action (fun (v:cases_pattern_expr) -> make ((p,v) :: env) tl)
    | Some (p, ETReference) :: tl -> (* non-terminal *)
        Gramext.action (fun (v:reference) ->
	  make ((p,CPatAtom (dummy_loc,Some v)) :: env) tl)
    | Some (p, ETIdent) :: tl -> (* non-terminal *)
        Gramext.action (fun (v:identifier) ->
	  make ((p,CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))) :: env) tl)
    | Some (p, ETBigint) :: tl -> (* non-terminal *)
        Gramext.action (fun (v:Bigint.bigint) ->
	  make ((p,CPatPrim (dummy_loc,Numeral v)) :: env) tl)
    | Some (p, ETConstrList _) :: tl ->
        Gramext.action (fun (v:cases_pattern_expr list) ->
          let dummyid = Ident (dummy_loc,id_of_string "_") in
	  make ((p,CPatCstr (dummy_loc,dummyid,v)) :: env) tl)
    | Some (p, (ETPattern | ETOther _)) :: tl -> 
	failwith "Unexpected entry of type cases pattern or other" in
  make [] (List.rev pil)

let make_constr_prod_item univ assoc from forpat = function
  | Term tok -> (Gramext.Stoken tok, None)
  | NonTerm (nt, ovar) ->
      let eobj = symbol_of_production assoc from forpat nt in
      (eobj, ovar)

let prepare_empty_levels entry (pos,p4assoc,name,reinit) =
  grammar_extend entry pos reinit [(name, p4assoc, [])]

let extend_constr entry (n,assoc,pos,p4assoc,name,reinit) mkact (forpat,pt) =
  let univ = get_univ "constr" in
  let pil = List.map (make_constr_prod_item univ assoc n forpat) pt in
  let (symbs,ntl) = List.split pil in
  let needed_levels = register_empty_levels forpat symbs in
  List.iter (prepare_empty_levels entry) needed_levels;
  grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact ntl])]

let extend_constr_notation (n,assoc,ntn,rule) =
  (* Add the notation in constr *)
  let mkact loc env = CNotation (loc,ntn,List.map snd env) in
  let (e,level) = get_constr_entry false (ETConstr (n,())) in
  let pos,p4assoc,name,reinit = find_position false assoc level in
  extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name,reinit)
    (make_constr_action mkact) (false,rule);
  (* Add the notation in cases_pattern *)
  let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in
  let (e,level) = get_constr_entry true (ETConstr (n,())) in
  let pos,p4assoc,name,reinit = find_position true assoc level in
  extend_constr e (ETConstr (n,()),assoc,pos,p4assoc,name,reinit)
    (make_cases_pattern_action mkact) (true,rule)

(**********************************************************************)
(** 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
    | [] -> 
	Gramext.action (fun loc -> f loc env)
    | None :: tl -> (* parse a non-binding item *)
        Gramext.action (fun _ -> make env tl)
    | Some (p, t) :: tl -> (* non-terminal *)
        Gramext.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_tactic_production =
  | TacTerm of string
  | TacNonTerm of
      loc * (Gram.te Gramext.g_symbol * argument_type) * string option

let make_prod_item = function
  | TacTerm s -> (Gramext.Stoken (Lexer.terminal s), None)
  | TacNonTerm (_,(nont,t), po) -> (nont, Option.map (fun p -> (p,t)) po)

(* Tactic grammar extensions *)

let tac_exts = ref []
let get_extend_tactic_grammars () = !tac_exts

let extend_tactic_grammar s gl =
  tac_exts := (s,gl) :: !tac_exts;
  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
  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 gl =
  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
  Gram.extend Vernac_.command None [(None, None, List.rev rules)]

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

(* Interpretation of the grammar entry names *)

let find_index s t =
  let t,n = repr_ident (id_of_string t) in
  if s <> t or n = None then raise Not_found;
  Option.get n

let rec interp_entry_name up_level s =
  let l = String.length s in
  if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
    let t, g = interp_entry_name up_level (String.sub s 3 (l-8)) in
    List1ArgType t, Gramext.Slist1 g
  else if l > 5 & String.sub s (l-5) 5 = "_list" then
    let t, g = interp_entry_name up_level (String.sub s 0 (l-5)) in
    List0ArgType t, Gramext.Slist0 g
  else if l > 4 & String.sub s (l-4) 4 = "_opt" then
    let t, g = interp_entry_name up_level (String.sub s 0 (l-4)) in
    OptArgType t, Gramext.Sopt g
  else
    let s = if s = "hyp" then "var" else s in
    try 
      let i = find_index "tactic" s in
      ExtraArgType s, 
      if up_level<>5 && i=up_level then Gramext.Sself else
      if up_level<>5 && i=up_level-1 then Gramext.Snext else
      Gramext.Snterml(Pcoq.Gram.Entry.obj Tactic.tactic_expr,string_of_int i)
    with Not_found ->
    let e = 
      (* Qualified entries are no longer in use *)
      try get_entry (get_univ "tactic") s
      with _ -> 
      try get_entry (get_univ "prim") s
      with _ ->
      try get_entry (get_univ "constr") s
      with _ -> error ("Unknown entry "^s)
    in
    let o = object_of_typed_entry e in
    let t = type_of_typed_entry e in
    t,Gramext.Snterm (Pcoq.Gram.Entry.obj o)

let make_vprod_item n = function
  | VTerm s -> (Gramext.Stoken (Lexer.terminal s), None)
  | VNonTerm (loc, nt, po) ->
      let (etyp, e) = interp_entry_name n nt in
      e, Option.map (fun p -> (p,etyp)) po

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 (Gramext.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 VTerm _::_ -> 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 mkprod = make_vprod_item 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) mkprod 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) mkprod prods in
  synchronize_level_positions ();
  grammar_extend entry pos None [(None, None, List.rev [rules])]

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

type notation_grammar = 
    int * Gramext.g_assoc option * notation * prod_item list

type all_grammar_command =
  | Notation of Notation.level * notation_grammar
  | TacticGrammar of
      (string * int * grammar_production list * 
        (Names.dir_path * Tacexpr.glob_tactic_expr))

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

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

let reset_extend_grammars_v8 () =
  let te = List.rev !tac_exts in
  let tv = List.rev !vernac_exts in
  tac_exts := [];
  vernac_exts := [];
  List.iter (fun (s,gl) -> print_string ("Resinstalling "^s); flush stdout; extend_tactic_grammar s gl) te;
  List.iter (fun (s,gl) -> extend_vernac_command_grammar s gl) tv

let recover_notation_grammar ntn prec =
  let l = map_succeed (function
    | Notation (prec',(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' -> 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 -> function
      | Notation _ -> n + 2 (* 1 for operconstr, 1 for pattern *)
      | TacticGrammar _ -> n + 1)
    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 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;
      survive_module = false;
      survive_section = false }