← Back to branch summary

~ubuntu-branches/debian/jessie/coq/jessie

« back to all changes in this revision

Viewing changes to parsing/egrammar.ml

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2011-12-25 13:46:09 UTC
  • mfrom: (1.3.6) (6.1.10 sid)
  • Revision ID: package-import@ubuntu.com-20111225134609-zwqkzmeni9g2xlq1
Tags: 8.3.pl3+dfsg-1
* New upstream release
  - remove all patches (applied upstream)

Show diffs side-by-side

added added

removed removed

Lines of Context:
parsing/egrammar.ml
1
1
(************************************************************************)
2
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
3
 
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 
3
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
4
4
(*   \VV/  **************************************************************)
5
5
(*    //   *      This file is distributed under the terms of the       *)
6
6
(*         *       GNU Lesser General Public License Version 2.1        *)
7
7
(************************************************************************)
8
8
 
9
 
(* $Id: egrammar.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
 
9
(* $Id: egrammar.ml 14779 2011-12-07 21:54:18Z herbelin $ *)
10
10
 
11
11
open Pp
12
12
open Util
169
169
      failwith "") symbs
170
170
 
171
171
let extend_constr (entry,level) (n,assoc) mkact forpat rules =
172
 
  List.iter (fun pt ->
 
172
  List.fold_left (fun nb pt ->
173
173
  let symbs = make_constr_prod_item assoc n forpat pt in
174
174
  let pure_sublevels = pure_sublevels level symbs in
175
175
  let needed_levels = register_empty_levels forpat pure_sublevels in
176
176
  let pos,p4assoc,name,reinit = find_position forpat assoc level in
 
177
  let nb_decls = List.length needed_levels + 1 in
177
178
  List.iter (prepare_empty_levels forpat) needed_levels;
178
 
  grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact pt])]) rules
 
179
  grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact pt])];
 
180
  nb_decls) 0 rules
179
181
 
180
182
let extend_constr_notation (n,assoc,ntn,rules) =
181
183
  (* Add the notation in constr *)
182
184
  let mkact loc env = CNotation (loc,ntn,env) in
183
185
  let e = interp_constr_entry_key false (ETConstr (n,())) in
184
 
  extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rules;
 
186
  let nb = extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rules in
185
187
  (* Add the notation in cases_pattern *)
186
188
  let mkact loc env = CPatNotation (loc,ntn,env) in
187
189
  let e = interp_constr_entry_key true (ETConstr (n,())) in
188
 
  extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact)
189
 
    true rules
 
190
  let nb' =
 
191
    extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact) true rules in
 
192
  nb+nb'
190
193
 
191
194
(**********************************************************************)
192
195
(** Making generic actions in type generic_argument                   *)
273
276
        (TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in
274
277
      make_rule univ (mkact key tac) make_prod_item prods in
275
278
  synchronize_level_positions ();
276
 
  grammar_extend entry pos None [(None, None, List.rev [rules])]
 
279
  grammar_extend entry pos None [(None, None, List.rev [rules])];
 
280
  1
277
281
 
278
282
(**********************************************************************)
279
283
(** State of the grammar extensions                                   *)
290
294
      (string * int * grammar_prod_item list *
291
295
         (dir_path * Tacexpr.glob_tactic_expr))
292
296
 
293
 
let (grammar_state : all_grammar_command list ref) = ref []
 
297
let (grammar_state : (int * all_grammar_command) list ref) = ref []
294
298
 
295
299
let extend_grammar gram =
296
 
  (match gram with
 
300
  let nb = match gram with
297
301
  | Notation (_,_,a) -> extend_constr_notation a
298
 
  | TacticGrammar g -> add_tactic_entry g);
299
 
  grammar_state := gram :: !grammar_state
 
302
  | TacticGrammar g -> add_tactic_entry g in
 
303
  grammar_state := (nb,gram) :: !grammar_state
300
304
 
301
305
let recover_notation_grammar ntn prec =
302
306
  let l = map_succeed (function
303
 
    | Notation (prec',vars,(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' ->
 
307
    | _, Notation (prec',vars,(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' ->
304
308
         vars, x
305
309
    | _ ->
306
310
         failwith "") !grammar_state in
320
324
  if l1 == l2 then ([], [], l1) else list_share_tails l1 l2
321
325
 
322
326
let number_of_entries gcl =
323
 
  List.fold_left
324
 
    (fun n -> function
325
 
      | Notation _ -> n + 2 (* 1 for operconstr, 1 for pattern *)
326
 
      | TacticGrammar _ -> n + 1)
327
 
    0 gcl
 
327
  List.fold_left (fun n (p,_) -> n + p) 0 gcl
328
328
 
329
329
let unfreeze (grams, lex) =
330
330
  let (undo, redo, common) = factorize_grams !grammar_state grams in
333
333
  remove_levels n;
334
334
  grammar_state := common;
335
335
  Lexer.unfreeze lex;
336
 
  List.iter extend_grammar (List.rev redo)
 
336
  List.iter extend_grammar (List.rev (List.map snd redo))
337
337
 
338
338
let init_grammar () =
339
339
  remove_grammars (number_of_entries !grammar_state);