Imported Upstream version 8.5~beta1+dfsg

1 files changed, 0 insertions, 368 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
deleted file mode 100644
index 6deb7622..00000000
--- a/parsing/egrammar.ml
+++ /dev/null
@@ -1,368 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
-(*   \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 check_cases_pattern_env loc (env,envlist,hasbinders) =
-  if hasbinders then error_invalid_pattern_notation loc else (env,envlist)
-
-let make_cases_pattern_action
-  (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil =
-  let rec make (env,envlist,hasbinders as fullenv) = function
-  | [] ->
-      Gram.action (fun loc -> f loc (check_cases_pattern_env 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, hasbinders) tl)
-    | ETReference ->
-        Gram.action (fun (v:reference) ->
-	  make (CPatAtom (dummy_loc,Some v) :: env, envlist, hasbinders) tl)
-    | ETName ->
-        Gram.action (fun (na:name located) ->
-	  make (cases_pattern_expr_of_name na :: env, envlist, hasbinders) tl)
-    | ETBigint ->
-        Gram.action (fun (v:Bigint.bigint) ->
-	  make (CPatPrim (dummy_loc,Numeral v) :: env, envlist, hasbinders) tl)
-    | ETConstrList (_,_) ->
-        Gram.action  (fun (vl:cases_pattern_expr list) ->
-	  make (env, vl :: envlist, hasbinders) tl)
-    | ETBinder _ | ETBinderList (true,_) ->
-	Gram.action (fun (v:local_binder list) ->
-	  make (env, envlist, hasbinders) tl)
-    | ETBinderList (false,_) ->
-	Gram.action (fun (v:local_binder list list) ->
-	  make (env, envlist, true) tl)
-    | (ETPattern | ETOther _) ->
-        anomaly "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,hasbinders) tl
-      else
-        make (env,heads::envlist,hasbinders) tl
-  in
-  make ([],[],false) (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 }
-
-let with_grammar_rule_protection f x =
-  let fs = freeze () in
-  try let a = f x in unfreeze fs; a
-  with reraise -> unfreeze fs; raise reraise