diff options
Diffstat (limited to 'parsing/pcoq.ml')
| -rw-r--r-- | parsing/pcoq.ml | 539 |
1 files changed, 160 insertions, 379 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 6dcf76da8c..efb89cd6e1 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -19,10 +19,19 @@ module G = GrammarMake (CLexer) let warning_verbose = Compat.warning_verbose -module Symbols = GramextMake(G) +let of_coq_assoc = function +| Extend.RightA -> CompatGramext.RightA +| Extend.LeftA -> CompatGramext.LeftA +| Extend.NonA -> CompatGramext.NonA + +let of_coq_position = function +| Extend.First -> CompatGramext.First +| Extend.Last -> CompatGramext.Last +| Extend.Before s -> CompatGramext.Before s +| Extend.After s -> CompatGramext.After s +| Extend.Level s -> CompatGramext.Level s -let gram_token_of_token = Symbols.stoken -let gram_token_of_string s = gram_token_of_token (CLexer.terminal s) +module Symbols = GramextMake(G) let camlp4_verbosity silent f x = let a = !warning_verbose in @@ -32,26 +41,6 @@ let camlp4_verbosity silent f x = let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x - -(** [grammar_object] is the superclass of all grammar entries *) - -module type Gramobj = -sig - type grammar_object - val weaken_entry : 'a G.entry -> grammar_object G.entry -end - -module Gramobj : Gramobj = -struct - type grammar_object = Obj.t - let weaken_entry e = Obj.magic e -end - -(** Grammar entries with associated types *) - -type grammar_object = Gramobj.grammar_object -let weaken_entry x = Gramobj.weaken_entry x - (** Grammar extensions *) (** NB: [extend_statment = @@ -63,14 +52,57 @@ let weaken_entry x = Gramobj.weaken_entry x In [single_extend_statement], first two parameters are name and assoc iff a level is created *) +(** Binding general entry keys to symbol *) + +let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> G.action = function +| Stop -> fun f -> G.action (fun loc -> f (to_coqloc loc)) +| Next (r, _) -> fun f -> G.action (fun x -> of_coq_action r (f x)) + +let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function + | Atoken t -> Symbols.stoken t + | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s) + | Alist1sep (s,sep) -> + Symbols.slist1sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep) + | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s) + | Alist0sep (s,sep) -> + Symbols.slist0sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep) + | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s) + | Aself -> Symbols.sself + | Anext -> Symbols.snext + | Aentry e -> + Symbols.snterm (G.Entry.obj e) + | Aentryl (e, n) -> + Symbols.snterml (G.Entry.obj e, string_of_int n) + | Arules rs -> + G.srules' (List.map symbol_of_rules rs) + +and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function +| Stop -> fun accu -> accu +| Next (r, s) -> fun accu -> symbol_of_rule r (symbol_of_prod_entry_key s :: accu) + +and symbol_of_rules : type a. a Extend.rules -> _ = function +| Rules (r, act) -> + let symb = symbol_of_rule r.norec_rule [] in + let act = of_coq_action r.norec_rule act in + (symb, act) + +let of_coq_production_rule : type a. a Extend.production_rule -> _ = function +| Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act) + +let of_coq_single_extend_statement (lvl, assoc, rule) = + (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule) + +let of_coq_extend_statement (pos, st) = + (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st) + (** Type of reinitialization data *) type gram_reinit = gram_assoc * gram_position +type extend_rule = +| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statment -> extend_rule + type ext_kind = - | ByGrammar of - grammar_object G.entry - * gram_reinit option (** for reinitialization if ever needed *) - * G.extend_statment + | ByGrammar of extend_rule | ByEXTEND of (unit -> unit) * (unit -> unit) (** The list of extensions *) @@ -86,13 +118,28 @@ let grammar_delete e reinit (pos,rls) = (List.rev rls); match reinit with | Some (a,ext) -> - let lev = match Option.map Compat.to_coq_position pos with - | Some (Level n) -> n + let a = of_coq_assoc a in + let ext = of_coq_position ext in + let lev = match pos with + | Some (CompatGramext.Level n) -> n | _ -> assert false in maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]]) | None -> () +(** Extension *) + +let grammar_extend e reinit ext = + let ext = of_coq_extend_statement ext in + let undo () = grammar_delete e reinit ext in + let redo () = camlp4_verbose (maybe_uncurry (G.extend e)) ext in + camlp4_state := ByEXTEND (undo, redo) :: !camlp4_state; + redo () + +let grammar_extend_sync e reinit ext = + camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state; + camlp4_verbose (maybe_uncurry (G.extend e)) (of_coq_extend_statement ext) + (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) @@ -119,12 +166,6 @@ module Gram = G.delete_rule e pil end -(** This extension command is used by the Grammar constr *) - -let unsafe_grammar_extend e reinit ext = - camlp4_state := ByGrammar (weaken_entry e,reinit,ext) :: !camlp4_state; - camlp4_verbose (maybe_uncurry (G.extend e)) ext - (** Remove extensions [n] is the number of extended entries (not the number of Grammar commands!) @@ -134,9 +175,8 @@ let rec remove_grammars n = if n>0 then (match !camlp4_state with | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove") - | ByGrammar(g,reinit,ext)::t -> - let f (a,b) = (of_coq_assoc a, of_coq_position b) in - grammar_delete g (Option.map f reinit) ext; + | ByGrammar (ExtendRule (g, reinit, ext)) :: t -> + grammar_delete g reinit (of_coq_extend_statement ext); camlp4_state := t; remove_grammars (n-1) | ByEXTEND (undo,redo)::t -> @@ -188,21 +228,9 @@ let get_univ u = if Hashtbl.mem utables u then u else raise Not_found -(** A table associating grammar to entries *) -let gtable : Obj.t Gram.entry String.Map.t ref = ref String.Map.empty - -let get_grammar (e : 'a Entry.t) : 'a Gram.entry = - Obj.magic (String.Map.find (Entry.repr e) !gtable) - -let set_grammar (e : 'a Entry.t) (g : 'a Gram.entry) = - assert (not (String.Map.mem (Entry.repr e) !gtable)); - gtable := String.Map.add (Entry.repr e) (Obj.magic g) !gtable - let new_entry u s = let ename = u ^ ":" ^ s in - let entry = Entry.create ename in let e = Gram.entry_create ename in - let () = set_grammar entry e in e let make_gen_entry u s = new_entry u s @@ -374,344 +402,97 @@ let main_entry = Vernac_.main_entry let set_command_entry e = Vernac_.command_entry_ref := e let get_command_entry () = !Vernac_.command_entry_ref -(**********************************************************************) -(* This determines (depending on the associativity of the current - level and on the expected associativity) if a reference to constr_n is - a reference to the current level (to be translated into "SELF" on the - left border and into "constr LEVEL n" elsewhere), to the level below - (to be translated into "NEXT") or to an below wrt associativity (to be - translated in camlp4 into "constr" without level) or to another level - (to be translated into "constr LEVEL n") - - The boolean is true if the entry was existing _and_ empty; this to - circumvent a weakness of camlp4/camlp5 whose undo mechanism is not the - converse of the extension mechanism *) - -let constr_level = string_of_int - -let default_levels = - [200,Extend.RightA,false; - 100,Extend.RightA,false; - 99,Extend.RightA,true; - 10,Extend.RightA,false; - 9,Extend.RightA,false; - 8,Extend.RightA,true; - 1,Extend.LeftA,false; - 0,Extend.RightA,false] - -let default_pattern_levels = - [200,Extend.RightA,true; - 100,Extend.RightA,false; - 99,Extend.RightA,true; - 11,Extend.LeftA,false; - 10,Extend.RightA,false; - 1,Extend.LeftA,false; - 0,Extend.RightA,false] - -let level_stack = - ref [(default_levels, default_pattern_levels)] - -(* At a same level, LeftA takes precedence over RightA and NoneA *) -(* In case, several associativity exists for a level, we make two levels, *) -(* first LeftA, then RightA and NoneA together *) - -let admissible_assoc = function - | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> false - | Extend.RightA, Some Extend.LeftA -> false - | _ -> true - -let create_assoc = function - | None -> Extend.RightA - | Some a -> a - -let error_level_assoc p current expected = - let pr_assoc = function - | Extend.LeftA -> str "left" - | Extend.RightA -> str "right" - | Extend.NonA -> str "non" in - errorlabstrm "" - (str "Level " ++ int p ++ str " is already declared " ++ - pr_assoc current ++ str " associative while it is now expected to be " ++ - pr_assoc expected ++ str " associative.") - -let create_pos = function - | None -> Extend.First - | Some lev -> Extend.After (constr_level lev) - -let find_position_gen forpat ensure assoc lev = - let ccurrent,pcurrent as current = List.hd !level_stack in - match lev with - | None -> - level_stack := current :: !level_stack; - None, None, None, None - | Some n -> - let after = ref None in - let init = ref None in - let rec add_level q = function - | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l - | (p,a,reinit)::l when Int.equal p n -> - if reinit then - let a' = create_assoc assoc in - (init := Some (a',create_pos q); (p,a',false)::l) - else if admissible_assoc (a,assoc) then - raise Exit - else - error_level_assoc p a (Option.get assoc) - | l -> after := q; (n,create_assoc assoc,ensure)::l - in - try - let updated = - if forpat then (ccurrent, add_level None pcurrent) - else (add_level None ccurrent, pcurrent) in - level_stack := updated:: !level_stack; - let assoc = create_assoc assoc in - begin match !init with - | None -> - (* Create the entry *) - Some (create_pos !after), Some assoc, Some (constr_level n), None - | _ -> - (* The reinit flag has been updated *) - Some (Extend.Level (constr_level n)), None, None, !init - end - with - (* Nothing has changed *) - Exit -> - level_stack := current :: !level_stack; - (* Just inherit the existing associativity and name (None) *) - Some (Extend.Level (constr_level n)), None, None, None - -let remove_levels n = - level_stack := List.skipn n !level_stack - -let rec list_mem_assoc_triple x = function - | [] -> false - | (a,b,c) :: l -> Int.equal a x || list_mem_assoc_triple x l - -let register_empty_levels forpat levels = - let filter n = - try - let levels = (if forpat then snd else fst) (List.hd !level_stack) in - if not (list_mem_assoc_triple n levels) then - Some (find_position_gen forpat true None (Some n)) - else None - with Failure _ -> None - in - List.map_filter filter levels - -let find_position forpat assoc level = - find_position_gen forpat false assoc level - -(* Synchronise the stack of level updates *) -let synchronize_level_positions () = - let _ = find_position true None None in () - -(**********************************************************************) -(* Binding constr entry keys to entries *) - -(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *) -let camlp4_assoc = function - | Some Extend.NonA | Some Extend.RightA -> Extend.RightA - | None | Some Extend.LeftA -> Extend.LeftA - -let assoc_eq al ar = match al, ar with -| Extend.NonA, Extend.NonA -| Extend.RightA, Extend.RightA -| Extend.LeftA, Extend.LeftA -> true -| _, _ -> false - -(* [adjust_level assoc from prod] where [assoc] and [from] are the name - and associativity of the level where to add the rule; the meaning of - the result is - - None = SELF - Some None = NEXT - Some (Some (n,cur)) = constr LEVEL n - s.t. if [cur] is set then [n] is the same as the [from] level *) -let adjust_level assoc from = function -(* Associativity is None means force the level *) - | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true)) -(* Compute production name on the right side *) - (* If NonA or LeftA on the right-hand side, set to NEXT *) - | (NumLevel n,BorderProd (Right,Some (Extend.NonA|Extend.LeftA))) -> - Some None - (* If RightA on the right-hand side, set to the explicit (current) level *) - | (NumLevel n,BorderProd (Right,Some Extend.RightA)) -> - Some (Some (n,true)) -(* Compute production name on the left side *) - (* If NonA on the left-hand side, adopt the current assoc ?? *) - | (NumLevel n,BorderProd (Left,Some Extend.NonA)) -> None - (* If the expected assoc is the current one, set to SELF *) - | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp4_assoc assoc) -> - None - (* Otherwise, force the level, n or n-1, according to expected assoc *) - | (NumLevel n,BorderProd (Left,Some a)) -> - begin match a with - | Extend.LeftA -> Some (Some (n, true)) - | _ -> Some None - end - (* None means NEXT *) - | (NextLevel,_) -> Some None -(* Compute production name elsewhere *) - | (NumLevel n,InternalProd) -> - match from with - | ETConstr (p,()) when Int.equal p (n + 1) -> Some None - | ETConstr (p,()) -> Some (Some (n, Int.equal n p)) - | _ -> Some (Some (n,false)) - -let compute_entry adjust forpat = function - | ETConstr (n,q) -> - (if forpat then weaken_entry Constr.pattern - else weaken_entry Constr.operconstr), - adjust (n,q), false - | ETName -> weaken_entry Prim.name, None, false - | ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList") - | ETBinder false -> weaken_entry Constr.binder, None, false - | ETBinderList (true,tkl) -> - let () = match tkl with [] -> () | _ -> assert false in - weaken_entry Constr.open_binders, None, false - | ETBinderList (false,_) -> anomaly (Pp.str "List of entries cannot be registered.") - | ETBigint -> weaken_entry Prim.bigint, None, false - | ETReference -> weaken_entry Constr.global, None, false - | ETPattern -> weaken_entry Constr.pattern, None, false - | ETConstrList _ -> anomaly (Pp.str "List of entries cannot be registered.") - | ETOther (u,n) -> assert false - -(* This computes the name of the level where to add a new rule *) -let interp_constr_entry_key forpat level = - if level = 200 && not forpat then weaken_entry Constr.binder_constr, None - else if forpat then weaken_entry Constr.pattern, Some level - else weaken_entry Constr.operconstr, Some level - -(* This computes the name to give to a production knowing the name and - associativity of the level where it must be added *) -let interp_constr_prod_entry_key ass from forpat en = - compute_entry (adjust_level ass from) forpat en - -(**********************************************************************) -(* Binding constr entry keys to symbols *) - -let is_self from e = - match from, e with - ETConstr(n,()), ETConstr(NumLevel n', - BorderProd(Right, _ (* Some(NonA|LeftA) *))) -> false - | ETConstr(n,()), ETConstr(NumLevel n',BorderProd(Left,_)) -> Int.equal n n' - | (ETName,ETName | ETReference, ETReference | ETBigint,ETBigint - | ETPattern, ETPattern) -> true - | ETOther(s1,s2), ETOther(s1',s2') -> - String.equal s1 s1' && String.equal s2 s2' - | _ -> false - -let is_binder_level from e = - match from, e with - ETConstr(200,()), - ETConstr(NumLevel 200,(BorderProd(Right,_)|InternalProd)) -> true - | _ -> false - -let make_sep_rules tkl = - Gram.srules' - [List.map gram_token_of_token tkl, - List.fold_right (fun _ v -> Gram.action (fun _ -> v)) tkl - (Gram.action (fun loc -> ()))] - -let rec symbol_of_constr_prod_entry_key assoc from forpat typ = - if is_binder_level from typ then - if forpat then - Symbols.snterml (Gram.Entry.obj Constr.pattern,"200") - else - Symbols.snterml (Gram.Entry.obj Constr.operconstr,"200") - else if is_self from typ then - Symbols.sself - else - match typ with - | ETConstrList (typ',[]) -> - Symbols.slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ')) - | ETConstrList (typ',tkl) -> - Symbols.slist1sep - (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'), - make_sep_rules tkl) - | ETBinderList (false,[]) -> - Symbols.slist1 - (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false)) - | ETBinderList (false,tkl) -> - Symbols.slist1sep - (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false), - make_sep_rules tkl) - - | _ -> - match interp_constr_prod_entry_key assoc from forpat typ with - | (eobj,None,_) -> Symbols.snterm (Gram.Entry.obj eobj) - | (eobj,Some None,_) -> Symbols.snext - | (eobj,Some (Some (lev,cur)),_) -> - Symbols.snterml (Gram.Entry.obj eobj,constr_level lev) - -(** Binding general entry keys to symbol *) - -let tuplify l = - List.fold_left (fun accu x -> Obj.repr (x, accu)) (Obj.repr ()) l - -let rec adj : type a b c. (a, b, Loc.t -> Loc.t * c) adj -> _ = function -| Adj0 -> Obj.magic (fun accu f loc -> f (Obj.repr (to_coqloc loc, tuplify accu))) -| AdjS e -> Obj.magic (fun accu f x -> adj e (x :: accu) f) - -let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function - | Atoken t -> Symbols.stoken t - | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s) - | Alist1sep (s,sep) -> - Symbols.slist1sep (symbol_of_prod_entry_key s, gram_token_of_string sep) - | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s) - | Alist0sep (s,sep) -> - Symbols.slist0sep (symbol_of_prod_entry_key s, gram_token_of_string sep) - | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s) - | Aself -> Symbols.sself - | Anext -> Symbols.snext - | Aentry e -> - let e = get_grammar e in - Symbols.snterm (Gram.Entry.obj (weaken_entry e)) - | Aentryl (e, n) -> - let e = get_grammar e in - Symbols.snterml (Gram.Entry.obj (weaken_entry e), string_of_int n) - | Arules rs -> Gram.srules' (symbol_of_rules rs [] (fun x -> I0 x)) - -and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function -| Stop -> fun accu -> accu -| Next (r, s) -> fun accu -> symbol_of_rule r (symbol_of_prod_entry_key s :: accu) +let epsilon_value f e = + let r = Rule (Next (Stop, e), fun x _ -> f x) in + let ext = of_coq_extend_statement (None, [None, None, [r]]) in + let entry = G.entry_create "epsilon" in + let () = maybe_uncurry (G.extend entry) ext in + try Some (parse_string entry "") with _ -> None -and symbol_of_rules : type a. a Extend.rules -> _ = function -| Rule0 -> fun accu _ -> accu -| RuleS (r, e, rs) -> fun accu f -> - let symb = symbol_of_rule r [] in - let act = adj e [] f in - symbol_of_rules rs ((symb, act) :: accu) (fun x -> IS (f x)) +(** Synchronized grammar extensions *) -let level_of_snterml e = int_of_string (Symbols.snterml_level e) +module GramState = Store.Make(struct end) -let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> Gram.action = function -| Stop -> fun f -> Gram.action (fun loc -> f (to_coqloc loc)) -| Next (r, _) -> fun f -> Gram.action (fun x -> of_coq_action r (f x)) +type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t -let of_coq_production_rule : type a. a Extend.production_rule -> _ = function -| Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act) +module GrammarCommand = Dyn.Make(struct end) +module GrammarInterp = struct type 'a t = 'a grammar_extension end +module GrammarInterpMap = GrammarCommand.Map(GrammarInterp) -let of_coq_single_extend_statement (lvl, assoc, rule) = - (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule) +let grammar_interp = ref GrammarInterpMap.empty -let of_coq_extend_statement (pos, st) = - (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st) - -let grammar_extend e reinit ext = - let ext = of_coq_extend_statement ext in - unsafe_grammar_extend e reinit ext +let (grammar_stack : (int * GrammarCommand.t * GramState.t) list ref) = ref [] -let name_of_entry e = Entry.unsafe_of_name (Gram.Entry.name e) +type 'a grammar_command = 'a GrammarCommand.tag -let list_entry_names () = [] +let create_grammar_command name interp : _ grammar_command = + let obj = GrammarCommand.create name in + let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in + obj -let epsilon_value f e = - let r = Rule (Next (Stop, e), fun x _ -> f x) in - let ext = of_coq_extend_statement (None, [None, None, [r]]) in - let entry = G.entry_create "epsilon" in - let () = maybe_uncurry (Gram.extend entry) ext in - try Some (parse_string entry "") with _ -> None +let extend_grammar_command tag g = + let modify = GrammarInterpMap.find tag !grammar_interp in + let grammar_state = match !grammar_stack with + | [] -> GramState.empty + | (_, _, st) :: _ -> st + in + let (rules, st) = modify g grammar_state in + let iter (ExtendRule (e, reinit, ext)) = grammar_extend_sync e reinit ext in + let () = List.iter iter rules in + let nb = List.length rules in + grammar_stack := (nb, GrammarCommand.Dyn (tag, g), st) :: !grammar_stack + +let recover_grammar_command (type a) (tag : a grammar_command) : a list = + let filter : _ -> a option = fun (_, GrammarCommand.Dyn (tag', v), _) -> + match GrammarCommand.eq tag tag' with + | None -> None + | Some Refl -> Some v + in + List.map_filter filter !grammar_stack + +let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar_command tag g + +(* 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 = (int * GrammarCommand.t * GramState.t) list * CLexer.frozen_t + +let freeze _ : frozen_t = (!grammar_stack, CLexer.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_stack grams in + let n = number_of_entries undo in + remove_grammars n; + grammar_stack := common; + CLexer.unfreeze lex; + List.iter extend_dyn_grammar (List.rev_map pi2 redo) + +(** No need to provide an init function : the grammar state is + statically available, and already empty initially, while + the lexer state should not be resetted, since it contains + keywords declared in g_*.ml4 *) + +let _ = + Summary.declare_summary "GRAMMAR_LEXER" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = Summary.nop } + +let with_grammar_rule_protection f x = + let fs = freeze false in + try let a = f x in unfreeze fs; a + with reraise -> + let reraise = Errors.push reraise in + let () = unfreeze fs in + iraise reraise (** Registering grammar of generic arguments *) |