diff options
Diffstat (limited to 'parsing/egrammar.ml')
| -rw-r--r-- | parsing/egrammar.ml | 420 |
1 files changed, 139 insertions, 281 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 09889d40..c723175c 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -6,64 +6,31 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: egrammar.ml,v 1.48.2.4 2005/12/23 22:16:46 herbelin Exp $ *) +(* $Id: egrammar.ml 7762 2005-12-30 10:55:33Z herbelin $ *) open Pp open Util -open Ppextend -open Extend open Pcoq +open Extend open Topconstr -open Ast open Genarg open Libnames open Nameops - -(* State of the grammar extensions *) - -type notation_grammar = - int * Gramext.g_assoc option * notation * prod_item list * int list option - -type all_grammar_command = - | Notation of (precedence * tolerability list) * notation_grammar - | Grammar of grammar_command - | TacticGrammar of - (string * (string * grammar_production list) * - (Names.dir_path * Tacexpr.raw_tactic_expr)) - list * (string * Genarg.argument_type list * - (string * Pptactic.grammar_terminals)) list - -let subst_all_grammar_command subst = function - | Notation _ -> anomaly "Notation not in GRAMMAR summary" - | Grammar gc -> Grammar (subst_grammar_command subst gc) - | TacticGrammar (g,p) -> TacticGrammar (g,p) (* TODO ... *) - -let (grammar_state : all_grammar_command list ref) = ref [] - +open Tacexpr +open Names +open Vernacexpr (**************************************************************************) -(* Interpretation of the right hand side of grammar rules *) - -(* When reporting errors, we add the name of the grammar rule that failed *) -let specify_name name e = - match e with - | UserError(lab,strm) -> - UserError(lab, (str"during interpretation of grammar rule " ++ - str name ++ str"," ++ spc () ++ strm)) - | Anomaly(lab,strm) -> - Anomaly(lab, (str"during interpretation of grammar rule " ++ - str name ++ str"," ++ spc () ++ strm)) - | Failure s -> - Failure("during interpretation of grammar rule "^name^", "^s) - | e -> e - -(* Translation of environments: a production +(* + * --- 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, - * make_act builds the following closure: + * the make_*_action family build the following closure: * * ((fun env -> * (fun vi -> @@ -77,11 +44,18 @@ let specify_name name e = * []) *) -open Names +(**********************************************************************) +(** 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_act (f : loc -> constr_expr action_env -> constr_expr) pil = +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) @@ -95,8 +69,8 @@ let make_act (f : loc -> constr_expr action_env -> constr_expr) pil = Gramext.action (fun (v:identifier) -> make ((p,CRef (Ident (dummy_loc,v))) :: env) tl) | Some (p, ETBigint) :: tl -> (* non-terminal *) - Gramext.action (fun (v:Bignat.bigint) -> - make ((p,CNumeral (dummy_loc,v)) :: env) tl) + 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 @@ -105,7 +79,7 @@ let make_act (f : loc -> constr_expr action_env -> constr_expr) pil = failwith "Unexpected entry of type cases pattern" in make [] (List.rev pil) -let make_act_in_cases_pattern (* For Notations *) +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 | [] -> @@ -121,8 +95,8 @@ let make_act_in_cases_pattern (* For Notations *) 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:Bignat.bigint) -> - make ((p,CPatNumeral (dummy_loc,v)) :: env) tl) + 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 @@ -131,183 +105,37 @@ let make_act_in_cases_pattern (* For Notations *) failwith "Unexpected entry of type cases pattern or other" in make [] (List.rev pil) -(* For V7 Grammar only *) -let make_cases_pattern_act - (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, ETPattern) :: tl -> (* non-terminal *) - Gramext.action (fun v -> make ((p,v) :: env) tl) - | Some (p, ETReference) :: tl -> (* non-terminal *) - Gramext.action (fun v -> make ((p,CPatAtom(dummy_loc,Some v)) :: env) - tl) - | Some (p, ETBigint) :: tl -> (* non-terminal *) - Gramext.action (fun v -> make ((p,CPatNumeral(dummy_loc,v)) :: env) tl) - | Some (p, (ETConstrList _ | ETIdent | ETConstr _ | ETOther _)) :: tl -> - error "ident and constr entry not admitted in patterns cases syntax extensions" in - make [] (List.rev pil) - -(* Grammar extension command. Rules are assumed correct. - * Type-checking of grammar rules is done during the translation of - * ast to the type grammar_command. We only check that the existing - * entries have the type assumed in the grammar command (these types - * annotations are added when type-checking the command, function - * Extend.of_ast) *) - -let symbol_of_prod_item univ assoc from forpat = function +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 coerce_to_id = function - | CRef (Ident (_,id)) -> id - | c -> - user_err_loc (constr_loc c, "subst_rawconstr", - str"This expression should be a simple identifier") - -let coerce_to_ref = function - | CRef r -> r - | c -> - user_err_loc (constr_loc c, "subst_rawconstr", - str"This expression should be a simple reference") - -let subst_ref loc subst id = - try coerce_to_ref (List.assoc id subst) with Not_found -> Ident (loc,id) - -let subst_pat_id loc subst id = - try List.assoc id subst - with Not_found -> CPatAtom (loc,Some (Ident (loc,id))) - -let subst_id subst id = - try coerce_to_id (List.assoc id subst) with Not_found -> id - -(* -let subst_cases_pattern_expr a loc subs = - let rec subst = function - | CPatAlias (_,p,x) -> CPatAlias (loc,subst p,x) - (* No subst in compound pattern ? *) - | CPatCstr (_,ref,pl) -> CPatCstr (loc,ref,List.map subst pl) - | CPatAtom (_,Some (Ident (_,id))) -> subst_pat_id loc subs id - | CPatAtom (_,x) -> CPatAtom (loc,x) - | CPatNotation (_,ntn,l) -> CPatNotation - | CPatNumeral (_,n) -> CPatNumeral (loc,n) - | CPatDelimiters (_,key,p) -> CPatDelimiters (loc,key,subst p) - in subst a -*) - -let subst_constr_expr a loc subs = - let rec subst = function - | CRef (Ident (_,id)) -> - (try List.assoc id subs with Not_found -> CRef (Ident (loc,id))) - (* Temporary: no robust treatment of substituted binders *) - | CLambdaN (_,[],c) -> subst c - | CLambdaN (_,([],t)::bl,c) -> subst (CLambdaN (loc,bl,c)) - | CLambdaN (_,((_,na)::bl,t)::bll,c) -> - let na = name_app (subst_id subs) na in - CLambdaN (loc,[[loc,na],subst t], subst (CLambdaN (loc,(bl,t)::bll,c))) - | CProdN (_,[],c) -> subst c - | CProdN (_,([],t)::bl,c) -> subst (CProdN (loc,bl,c)) - | CProdN (_,((_,na)::bl,t)::bll,c) -> - let na = name_app (subst_id subs) na in - CProdN (loc,[[loc,na],subst t], subst (CProdN (loc,(bl,t)::bll,c))) - | CLetIn (_,(_,na),b,c) -> - let na = name_app (subst_id subs) na in - CLetIn (loc,(loc,na),subst b,subst c) - | CArrow (_,a,b) -> CArrow (loc,subst a,subst b) - | CAppExpl (_,(p,Ident (_,id)),l) -> - CAppExpl (loc,(p,subst_ref loc subs id),List.map subst l) - | CAppExpl (_,r,l) -> CAppExpl (loc,r,List.map subst l) - | CApp (_,(p,a),l) -> - CApp (loc,(p,subst a),List.map (fun (a,i) -> (subst a,i)) l) - | CCast (_,a,b) -> CCast (loc,subst a,subst b) - | CNotation (_,n,l) -> CNotation (loc,n,List.map subst l) - | CDelimiters (_,s,a) -> CDelimiters (loc,s,subst a) - | CHole _ | CEvar _ | CPatVar _ | CSort _ - | CNumeral _ | CDynamic _ | CRef _ as x -> x - | CCases (_,(po,rtntypo),a,bl) -> - (* TODO: apply g on the binding variables in pat... *) - let bl = List.map (fun (_,pat,rhs) -> (loc,pat,subst rhs)) bl in - CCases (loc,(option_app subst po,option_app subst rtntypo), - List.map (fun (tm,x) -> subst tm,x) a,bl) - | COrderedCase (_,s,po,a,bl) -> - COrderedCase (loc,s,option_app subst po,subst a,List.map subst bl) - | CLetTuple (_,nal,(na,po),a,b) -> - let na = option_app (name_app (subst_id subs)) na in - let nal = List.map (name_app (subst_id subs)) nal in - CLetTuple (loc,nal,(na,option_app subst po),subst a,subst b) - | CIf (_,c,(na,po),b1,b2) -> - let na = option_app (name_app (subst_id subs)) na in - CIf (loc,subst c,(na,option_app subst po),subst b1,subst b2) - | CFix (_,id,dl) -> - CFix (loc,id,List.map (fun (id,n,bl, t,d) -> - (id,n, - List.map(function - LocalRawAssum(nal,ty) -> LocalRawAssum(nal,subst ty) - | LocalRawDef(na,def) -> LocalRawDef(na,subst def)) bl, - subst t,subst d)) dl) - | CCoFix (_,id,dl) -> - CCoFix (loc,id,List.map (fun (id,bl,t,d) -> - (id, - List.map(function - LocalRawAssum(nal,ty) -> LocalRawAssum(nal,subst ty) - | LocalRawDef(na,def) -> LocalRawDef(na,subst def)) bl, - subst t,subst d)) dl) - in subst a - -(* For V7 Grammar only *) -let make_rule univ assoc etyp rule = - if not !Options.v7 then anomaly "No Grammar in new syntax"; - let pil = List.map (symbol_of_prod_item univ assoc etyp false) rule.gr_production in +let extend_constr entry (n,assoc,pos,p4assoc,name) 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 act = match etyp with - | ETPattern -> - (* Ugly *) - let f loc env = match rule.gr_action, env with - | CRef (Ident(_,p)), [p',a] when p=p' -> a - | CDelimiters (_,s,CRef (Ident(_,p))), [p',a] when p=p' -> - CPatDelimiters (loc,s,a) - | _ -> error "Unable to handle this grammar extension of pattern" in - make_cases_pattern_act f ntl - | ETConstrList _ | ETIdent | ETBigint | ETReference -> error "Cannot extend" - | ETConstr _ | ETOther _ -> - make_act (subst_constr_expr rule.gr_action) ntl in - (symbs, act) + grammar_extend entry pos [(name, p4assoc, [symbs, mkact ntl])] -(* Rules of a level are entered in reverse order, so that the first rules - are applied before the last ones *) -(* For V7 Grammar only *) -let extend_entry univ (te, etyp, pos, name, ass, p4ass, rls) = - let rules = List.rev (List.map (make_rule univ ass etyp) rls) in - grammar_extend te pos [(name, p4ass, rules)] - -(* Defines new entries. If the entry already exists, check its type *) -let define_entry univ {ge_name=typ; gl_assoc=ass; gl_rules=rls} = - let e,lev,keepassoc = get_constr_entry false typ in - let pos,p4ass,name = find_position false keepassoc ass lev in - (e,typ,pos,name,ass,p4ass,rls) - -(* Add a bunch of grammar rules. Does not check if it is well formed *) -(* For V7 Grammar only *) -let extend_grammar_rules gram = - let univ = get_univ gram.gc_univ in - let tl = List.map (define_entry univ) gram.gc_entries in - List.iter (extend_entry univ) tl - -(* Add a grammar rules for tactics *) -type grammar_tactic_production = - | TacTerm of string - | TacNonTerm of loc * (Gram.te Gramext.g_symbol * argument_type) * string option +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,keepassoc) = get_constr_entry false (ETConstr (n,())) in + let pos,p4assoc,name = find_position false keepassoc assoc level in + extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name) + (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,keepassoc) = get_constr_entry true (ETConstr (n,())) in + let pos,p4assoc,name = find_position true keepassoc assoc level in + extend_constr e (ETConstr (n,()),assoc,pos,p4assoc,name) + (make_cases_pattern_action mkact) (true,rule) -let make_prod_item = function - | TacTerm s -> (Gramext.Stoken (Extend.terminal s), None) - | TacNonTerm (_,(nont,t), po) -> - (nont, option_app (fun p -> (p,t)) po) +(**********************************************************************) +(** Making generic actions in type generic_argument *) -let make_gen_act f pil = +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) @@ -317,73 +145,77 @@ let make_gen_act f pil = Gramext.action (fun v -> make ((p,in_generic t v) :: env) tl) in make [] (List.rev pil) -let extend_constr entry (n,assoc,pos,p4assoc,name) make_act (forpat,pt) = - let univ = get_univ "constr" in - let pil = List.map (symbol_of_prod_item univ assoc n forpat) pt in - let (symbs,ntl) = List.split pil in - let act = make_act ntl in - grammar_extend entry pos [(name, p4assoc, [symbs, act])] - -let extend_constr_notation (n,assoc,ntn,rule,permut) = - let mkact = - match permut with - None -> (fun loc env -> CNotation (loc,ntn,List.map snd env)) - | Some p -> (fun loc env -> - CNotation (loc,ntn,List.map (fun i -> snd (List.nth env i)) p)) in - let (e,level,keepassoc) = get_constr_entry false (ETConstr (n,())) in - let pos,p4assoc,name = find_position false keepassoc assoc level in - extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name) - (make_act mkact) (false,rule); - if not !Options.v7 then - let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in - let (e,level,keepassoc) = get_constr_entry true (ETConstr (n,())) in - let pos,p4assoc,name = find_position true keepassoc assoc level in - extend_constr e (ETConstr (n,()),assoc,pos,p4assoc,name) - (make_act_in_cases_pattern mkact) (true,rule) - -(* These grammars are not a removable *) -let make_rule univ f g (s,pt) = - let hd = Gramext.Stoken ("IDENT", s) in - let pil = (hd,None) :: List.map g pt in - let (symbs,ntl) = List.split pil in - let act = make_gen_act f ntl in +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_app (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 make_act loc l = Tacexpr.TacExtend (loc,s,List.map snd l) in - let rules = List.map (make_rule univ make_act make_prod_item) gl 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 make_act loc l = Vernacexpr.VernacExtend (s,List.map snd l) in - let rules = List.map (make_rule univ make_act make_prod_item) gl 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)] -let rec interp_entry_name u s = +(**********************************************************************) +(** 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; + out_some n + +let rec interp_entry_name up_level u 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 u (String.sub s 3 (l-8)) in + let t, g = interp_entry_name up_level u (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 u (String.sub s 0 (l-5)) in + let t, g = interp_entry_name up_level u (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 u (String.sub s 0 (l-4)) in + let t, g = interp_entry_name up_level u (String.sub s 0 (l-4)) in OptArgType t, Gramext.Sopt g else + try + let i = find_index "tactic" s in + TacticArgType i, + if i=up_level then Gramext.Sself else + if 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 = - if !Options.v7 then get_entry (get_univ u) s - else (* Qualified entries are no longer in use *) try get_entry (get_univ "tactic") s with _ -> @@ -396,31 +228,61 @@ let rec interp_entry_name u s = let t = type_of_typed_entry e in t,Gramext.Snterm (Pcoq.Gram.Entry.obj o) -let qualified_nterm current_univ = function - | NtQual (univ, en) -> if !Options.v7 then (univ, en) else assert false - | NtShort en -> (current_univ, en) - -let make_vprod_item univ = function - | VTerm s -> (Gramext.Stoken (Extend.terminal s), None) +let make_vprod_item n univ = function + | VTerm s -> (Gramext.Stoken (Lexer.terminal s), None) | VNonTerm (loc, nt, po) -> - let (u,nt) = qualified_nterm univ nt in - let (etyp, e) = interp_entry_name u nt in + let (etyp, e) = interp_entry_name n univ nt in e, option_app (fun p -> (p,etyp)) po -let add_tactic_entries gl = +let get_tactic_entry n = + if n = 0 then + weaken_entry Tactic.simple_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 make_act s tac loc l = Tacexpr.TacAlias (loc,s,l,tac) in - let f (s,l,tac) = - make_rule univ (make_act s tac) (make_vprod_item "tactic") l in - let rules = List.map f gl in + let entry, pos = get_tactic_entry lev in + let mkprod = make_vprod_item lev "tactic" 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 let _ = find_position true true None None (* to synchronise with remove *) in - grammar_extend Tactic.simple_tactic None [(None, None, List.rev rules)] + grammar_extend entry pos [(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 - | Grammar g -> extend_grammar_rules g - | TacticGrammar (l,_) -> add_tactic_entries l); + | TacticGrammar g -> add_tactic_entry g); grammar_state := gram :: !grammar_state let reset_extend_grammars_v8 () = @@ -428,12 +290,12 @@ let reset_extend_grammars_v8 () = let tv = List.rev !vernac_exts in tac_exts := []; vernac_exts := []; - List.iter (fun (s,gl) -> extend_tactic_grammar s gl) te; + 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 + | Notation (prec',(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' -> x | _ -> failwith "") !grammar_state in assert (List.length l = 1); List.hd l @@ -453,11 +315,7 @@ let factorize_grams l1 l2 = let number_of_entries gcl = List.fold_left (fun n -> function - | Notation _ -> - if !Options.v7 then n + 1 - else n + 2 (* 1 for operconstr, 1 for pattern *) - | Grammar gc -> - n + (List.length gc.gc_entries) + | Notation _ -> n + 2 (* 1 for operconstr, 1 for pattern *) | TacticGrammar _ -> n + 1) 0 gcl |