diff options
Diffstat (limited to 'parsing/egrammar.ml')
| -rw-r--r-- | parsing/egrammar.ml | 100 |
1 files changed, 50 insertions, 50 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index ba965a54..4418a45f 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -1,14 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) (************************************************************************) -(* $Id: egrammar.ml 14779 2011-12-07 21:54:18Z herbelin $ *) - open Pp +open Compat open Util open Pcoq open Extend @@ -57,45 +56,43 @@ let cases_pattern_expr_of_name (loc,na) = match na with | Name id -> CPatAtom (loc,Some (Ident (loc,id))) type grammar_constr_prod_item = - | GramConstrTerminal of Token.pattern + | 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 *) -type 'a action_env = 'a list * 'a list list - let make_constr_action (f : loc -> constr_notation_substitution -> constr_expr) pil = let rec make (constrs,constrlists,binders as fullsubst) = function | [] -> - Gramext.action (fun loc -> f loc fullsubst) + Gram.action (fun loc -> f loc fullsubst) | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl -> (* parse a non-binding item *) - Gramext.action (fun _ -> make fullsubst tl) + Gram.action (fun _ -> make fullsubst tl) | GramConstrNonTerminal (typ, Some _) :: tl -> (* parse a binding non-terminal *) - (match typ with - | (ETConstr _| ETOther _) -> - Gramext.action (fun (v:constr_expr) -> + (match typ with + | (ETConstr _| ETOther _) -> + Gram.action (fun (v:constr_expr) -> make (v :: constrs, constrlists, binders) tl) - | ETReference -> - Gramext.action (fun (v:reference) -> + | ETReference -> + Gram.action (fun (v:reference) -> make (CRef v :: constrs, constrlists, binders) tl) - | ETName -> - Gramext.action (fun (na:name located) -> + | ETName -> + Gram.action (fun (na:name located) -> make (constr_expr_of_name na :: constrs, constrlists, binders) tl) - | ETBigint -> - Gramext.action (fun (v:Bigint.bigint) -> + | ETBigint -> + Gram.action (fun (v:Bigint.bigint) -> make (CPrim(dummy_loc,Numeral v) :: constrs, constrlists, binders) tl) - | ETConstrList (_,n) -> - Gramext.action (fun (v:constr_expr list) -> + | ETConstrList (_,n) -> + Gram.action (fun (v:constr_expr list) -> make (constrs, v::constrlists, binders) tl) | ETBinder _ | ETBinderList (true,_) -> - Gramext.action (fun (v:local_binder list) -> + Gram.action (fun (v:local_binder list) -> make (constrs, constrlists, v::binders) tl) | ETBinderList (false,_) -> - Gramext.action (fun (v:local_binder list list) -> + Gram.action (fun (v:local_binder list list) -> make (constrs, constrlists, List.flatten v::binders) tl) | ETPattern -> failwith "Unexpected entry of type cases pattern") @@ -113,26 +110,26 @@ let make_cases_pattern_action (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil = let rec make (env,envlist as fullenv) = function | [] -> - Gramext.action (fun loc -> f loc fullenv) + Gram.action (fun loc -> f loc fullenv) | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl -> (* parse a non-binding item *) - Gramext.action (fun _ -> make fullenv tl) + Gram.action (fun _ -> make fullenv tl) | GramConstrNonTerminal (typ, Some _) :: tl -> (* parse a binding non-terminal *) (match typ with | ETConstr _ -> (* pattern non-terminal *) - Gramext.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl) + Gram.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl) | ETReference -> - Gramext.action (fun (v:reference) -> + Gram.action (fun (v:reference) -> make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl) | ETName -> - Gramext.action (fun (na:name located) -> + Gram.action (fun (na:name located) -> make (cases_pattern_expr_of_name na :: env, envlist) tl) | ETBigint -> - Gramext.action (fun (v:Bigint.bigint) -> + Gram.action (fun (v:Bigint.bigint) -> make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl) | ETConstrList (_,_) -> - Gramext.action (fun (vl:cases_pattern_expr list) -> + 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") @@ -146,7 +143,7 @@ let make_cases_pattern_action let rec make_constr_prod_item assoc from forpat = function | GramConstrTerminal tok :: l -> - Gramext.Stoken tok :: make_constr_prod_item assoc from forpat 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 @@ -156,17 +153,18 @@ let rec make_constr_prod_item assoc from forpat = function [] let prepare_empty_levels forpat (pos,p4assoc,name,reinit) = - let entry = + let entry = if forpat then weaken_entry Constr.pattern else weaken_entry Constr.operconstr in - grammar_extend entry pos reinit [(name, p4assoc, [])] + grammar_extend entry reinit (pos,[(name, p4assoc, [])]) let pure_sublevels level symbs = - map_succeed (function - | Gramext.Snterml (_,n) when Some (int_of_string n) <> level -> - int_of_string n - | _ -> - failwith "") 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 -> @@ -176,7 +174,7 @@ let extend_constr (entry,level) (n,assoc) mkact forpat rules = 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 pos reinit [(name, p4assoc, [symbs, mkact pt])]; + grammar_extend entry reinit (pos,[(name, p4assoc, [symbs, mkact pt])]); nb_decls) 0 rules let extend_constr_notation (n,assoc,ntn,rules) = @@ -187,8 +185,8 @@ let extend_constr_notation (n,assoc,ntn,rules) = (* 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 + let nb' = extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact) + true rules in nb+nb' (**********************************************************************) @@ -198,11 +196,11 @@ 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) + Gram.action (fun loc -> f loc env) | None :: tl -> (* parse a non-binding item *) - Gramext.action (fun _ -> make env tl) + Gram.action (fun _ -> make env tl) | Some (p, t) :: tl -> (* non-terminal *) - Gramext.action (fun v -> make ((p,in_generic t v) :: env) tl) in + Gram.action (fun v -> make ((p,in_generic t v) :: env) tl) in make [] (List.rev pil) let make_rule univ f g pt = @@ -216,10 +214,10 @@ let make_rule univ f g pt = type grammar_prod_item = | GramTerminal of string | GramNonTerminal of - loc * argument_type * Gram.te prod_entry_key * identifier option + loc * argument_type * prod_entry_key * identifier option let make_prod_item = function - | GramTerminal s -> (Gramext.Stoken (Lexer.terminal s), None) + | 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) @@ -229,19 +227,21 @@ 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 - Gram.extend Tactic.simple_tactic None [(None, None, List.rev rules)] + 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 gl = +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 - Gram.extend Vernac_.command None [(None, None, List.rev rules)] + maybe_uncurry (Gram.extend nt) (None,[(None, None, List.rev rules)]) (**********************************************************************) (** Grammar declaration for Tactic Notation (Coq level) *) @@ -252,7 +252,7 @@ let get_tactic_entry n = 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)) + weaken_entry Tactic.tactic_expr, Some (Compat.Level (string_of_int n)) else error ("Invalid Tactic Notation level: "^(string_of_int n)^".") @@ -276,14 +276,14 @@ let add_tactic_entry (key,lev,prods,tac) = (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 pos None [(None, None, List.rev [rules])]; + grammar_extend entry None (pos,[(None, None, List.rev [rules])]); 1 (**********************************************************************) (** State of the grammar extensions *) type notation_grammar = - int * Gramext.g_assoc option * notation * grammar_constr_prod_item list list + int * gram_assoc option * notation * grammar_constr_prod_item list list type all_grammar_command = | Notation of |