diff options
| -rw-r--r-- | grammar/tacextend.ml4 | 4 | ||||
| -rw-r--r-- | parsing/egramcoq.ml | 97 | ||||
| -rw-r--r-- | parsing/egramcoq.mli | 19 | ||||
| -rw-r--r-- | printing/pptactic.ml | 10 | ||||
| -rw-r--r-- | printing/pptactic.mli | 9 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 207 |
6 files changed, 224 insertions, 122 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index ce97ee78e..f11927e77 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -124,7 +124,9 @@ let make_one_printing_rule se (pt,e) = let level = mlexpr_of_int 0 in (* only level 0 supported here *) let loc = MLast.loc_of_expr e in let prods = mlexpr_of_list mlexpr_terminals_of_grammar_tactic_prod_item_expr pt in - <:expr< ($se$, $make_tags loc pt$, ($level$, $prods$)) >> + <:expr< { Pptactic.pptac_key = $se$; + pptac_args = $make_tags loc pt$; + pptac_prods = ($level$, $prods$) } >> let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se) diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 8f1fda02b..762379803 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -194,17 +194,33 @@ let extend_constr (entry,level) (n,assoc) mkact forpat rules = [(name, Option.map of_coq_assoc p4assoc, [symbs, mkact pt])]); nb_decls) 0 rules -let extend_constr_notation (n,assoc,ntn,rules) = +type notation_grammar = { + notgram_level : int; + notgram_assoc : gram_assoc option; + notgram_notation : notation; + notgram_prods : grammar_constr_prod_item list list +} + +let extend_constr_constr_notation ng = + let level = ng.notgram_level in + let mkact loc env = CNotation (loc, ng.notgram_notation, env) in + let e = interp_constr_entry_key false (ETConstr (level, ())) in + let ext = (ETConstr (level, ()), ng.notgram_assoc) in + extend_constr e ext (make_constr_action mkact) false ng.notgram_prods + +let extend_constr_pat_notation ng = + let level = ng.notgram_level in + let mkact loc env = CPatNotation (loc, ng.notgram_notation, env, []) in + let e = interp_constr_entry_key true (ETConstr (level, ())) in + let ext = ETConstr (level, ()), ng.notgram_assoc in + extend_constr e ext (make_cases_pattern_action mkact) true ng.notgram_prods + +let extend_constr_notation ng = (* 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 + let nb = extend_constr_constr_notation ng 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' + let nb' = extend_constr_pat_notation ng in + nb + nb' (**********************************************************************) (** Grammar declaration for Tactic Notation (Coq level) *) @@ -219,43 +235,46 @@ let get_tactic_entry 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 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 (mkact key tac) prods - end - else - let mkact s tac loc l = - (TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in - make_rule (mkact key tac) prods in - synchronize_level_positions (); - grammar_extend entry None (Option.map of_coq_position 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 tactic_grammar = { + tacgram_key : string; + tacgram_level : int; + tacgram_prods : grammar_prod_item list; + tacgram_tactic : dir_path * Tacexpr.glob_tactic_expr; +} 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)) + | TacticGrammar of tactic_grammar + +(* Declaration of the tactic grammar rule *) + +let head_is_ident tg = match tg.tacgram_prods with +| GramTerminal _::_ -> true +| _ -> false + +let add_tactic_entry tg = + let entry, pos = get_tactic_entry tg.tacgram_level in + let rules = + if tg.tacgram_level = 0 then begin + if not (head_is_ident tg) then + error "Notation for simple tactic must start with an identifier."; + let mkact loc l = + (TacAlias (loc,tg.tacgram_key,l,tg.tacgram_tactic):raw_atomic_tactic_expr) in + make_rule mkact tg.tacgram_prods + end + else + let mkact loc l = + (TacAtom(loc,TacAlias(loc,tg.tacgram_key,l,tg.tacgram_tactic)):raw_tactic_expr) in + make_rule mkact tg.tacgram_prods in + synchronize_level_positions (); + grammar_extend entry None (Option.map of_coq_position pos,[(None, None, List.rev [rules])]); + 1 let (grammar_state : (int * all_grammar_command) list ref) = ref [] @@ -267,8 +286,8 @@ let extend_grammar gram = let recover_notation_grammar ntn prec = let filter = function - | _, Notation (prec', vars, (_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' -> - Some (vars, x) + | _, Notation (prec', vars, ng) when prec = prec' & ntn = ng.notgram_notation -> + Some (vars, ng) | _ -> None in let l = List.map_filter filter !grammar_state in assert (List.length l = 1); diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 0bd8d1990..3079ffc28 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -32,8 +32,19 @@ type grammar_constr_prod_item = (* tells action rule to make a list of the n previous parsed items; concat with last parsed list if true *) -type notation_grammar = - int * Extend.gram_assoc option * notation * grammar_constr_prod_item list list +type notation_grammar = { + notgram_level : int; + notgram_assoc : gram_assoc option; + notgram_notation : notation; + notgram_prods : grammar_constr_prod_item list list +} + +type tactic_grammar = { + tacgram_key : string; + tacgram_level : int; + tacgram_prods : grammar_prod_item list; + tacgram_tactic : dir_path * Tacexpr.glob_tactic_expr; +} (** Adding notations *) @@ -44,9 +55,7 @@ type all_grammar_command = (** not needed for defining grammar, hosted by egrammar for transmission to interp_aconstr (via recover_notation_grammar) *) * notation_grammar - | TacticGrammar of - (string * int * grammar_prod_item list * - (dir_path * Tacexpr.glob_tactic_expr)) + | TacticGrammar of tactic_grammar val extend_grammar : all_grammar_command -> unit diff --git a/printing/pptactic.ml b/printing/pptactic.ml index d16035fba..b790c4ea6 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -28,11 +28,17 @@ let pr_global x = Nametab.pr_global_env Idset.empty x type grammar_terminals = string option list +type pp_tactic = { + pptac_key : string; + pptac_args : argument_type list; + pptac_prods : int * grammar_terminals; +} + (* Extensions *) let prtac_tab = Hashtbl.create 17 -let declare_extra_tactic_pprule (s,tags,prods) = - Hashtbl.add prtac_tab (s,tags) prods +let declare_extra_tactic_pprule pt = + Hashtbl.add prtac_tab (pt.pptac_key, pt.pptac_args) (pt.pptac_prods) let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab (s,tags) diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 249a4a0af..61acffd08 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -47,9 +47,14 @@ val declare_extra_genarg_pprule : type grammar_terminals = string option list +type pp_tactic = { + pptac_key : string; + pptac_args : argument_type list; + pptac_prods : int * grammar_terminals; +} + (** if the boolean is false then the extension applies only to old syntax *) -val declare_extra_tactic_pprule : - string * argument_type list * (int * grammar_terminals) -> unit +val declare_extra_tactic_pprule : pp_tactic -> unit val exists_extra_tactic_pprule : string -> argument_type list -> bool diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index d406bf8d9..a67400788 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -62,24 +62,26 @@ let rec make_tags = function | GramNonTerminal (loc, etyp, _, po) :: l -> etyp :: make_tags l | [] -> [] -let cache_tactic_notation (_,(local,pa,pp)) = - Egramcoq.extend_grammar (Egramcoq.TacticGrammar pa); - Pptactic.declare_extra_tactic_pprule pp +type tactic_grammar_obj = { + tacobj_local : locality_flag; + tacobj_tacgram : tactic_grammar; + tacobj_tacpp : Pptactic.pp_tactic; +} -let subst_tactic_parule subst (key,n,p,(d,tac)) = - (key,n,p,(d,Tacinterp.subst_tactic subst tac)) +let cache_tactic_notation (_, tobj) = + Egramcoq.extend_grammar (Egramcoq.TacticGrammar tobj.tacobj_tacgram); + Pptactic.declare_extra_tactic_pprule tobj.tacobj_tacpp -let subst_tactic_notation (subst,(local,pa,pp)) = - (local,subst_tactic_parule subst pa,pp) +let subst_tactic_parule subst tg = + let dir, tac = tg.tacgram_tactic in + { tg with tacgram_tactic = (dir, Tacinterp.subst_tactic subst tac); } -let classify_tactic_notation (local,_,_ as o) = - if local then Dispose else Substitute o +let subst_tactic_notation (subst, tobj) = + { tobj with + tacobj_tacgram = subst_tactic_parule subst tobj.tacobj_tacgram; } -type tactic_grammar_obj = - locality_flag - * (string * int * grammar_prod_item list * - (dir_path * Tacexpr.glob_tactic_expr)) - * (string * Genarg.argument_type list * (int * Pptactic.grammar_terminals)) +let classify_tactic_notation tacobj = + if tacobj.tacobj_local then Dispose else Substitute tacobj let inTacticGrammar : tactic_grammar_obj -> obj = declare_object {(default_object "TacticGrammar") with @@ -105,11 +107,25 @@ let add_tactic_notation (local,n,prods,e) = let prods = List.map (interp_prod_item n) prods in let tags = make_tags prods in let key = next_key_away (tactic_notation_key prods) tags in - let pprule = (key,tags,(n,List.map make_terminal_status prods)) in + let pprule = { + Pptactic.pptac_key = key; + pptac_args = tags; + pptac_prods = (n, List.map make_terminal_status prods); + } in let ids = List.fold_left cons_production_parameter [] prods in let tac = Tacinterp.glob_tactic_env ids (Global.env()) e in - let parule = (key,n,prods,(Lib.cwd(),tac)) in - Lib.add_anonymous_leaf (inTacticGrammar (local,parule,pprule)) + let parule = { + tacgram_key = key; + tacgram_level = n; + tacgram_prods = prods; + tacgram_tactic = (Lib.cwd (), tac); + } in + let tacobj = { + tacobj_local = local; + tacobj_tacgram = parule; + tacobj_tacpp = pprule; + } in + Lib.add_anonymous_leaf (inTacticGrammar tacobj) (**********************************************************************) (* Printing grammar entries *) @@ -702,7 +718,19 @@ let error_incompatible_level ntn oldprec prec = spc() ++ str "while it is now required to be" ++ spc() ++ pr_level ntn prec ++ str ".") -let cache_one_syntax_extension (typs,prec,ntn,gr,pp) = +type syntax_extension = { + synext_intern : notation_var_internalization_type list; + synext_level : Notation.level; + synext_notation : notation; + synext_notgram : notation_grammar; + synext_unparsing : unparsing list; +} + +type syntax_extension_obj = locality_flag * syntax_extension list + +let cache_one_syntax_extension se = + let ntn = se.synext_notation in + let prec = se.synext_level in try let oldprec = Notation.level_of_notation ntn in if prec <> oldprec then error_incompatible_level ntn oldprec prec @@ -710,34 +738,30 @@ let cache_one_syntax_extension (typs,prec,ntn,gr,pp) = (* Reserve the notation level *) Notation.declare_notation_level ntn prec; (* Declare the parsing rule *) - Egramcoq.extend_grammar (Egramcoq.Notation (prec,typs,gr)); + Egramcoq.extend_grammar (Egramcoq.Notation (prec, se.synext_intern, se.synext_notgram)); (* Declare the printing rule *) - Notation.declare_notation_printing_rule ntn (pp,fst prec) + Notation.declare_notation_printing_rule ntn (se.synext_unparsing, fst prec) -let cache_syntax_extension (_,(_,sy_rules)) = - List.iter cache_one_syntax_extension sy_rules +let cache_syntax_extension (_, (_, sy)) = + List.iter cache_one_syntax_extension sy let subst_parsing_rule subst x = x let subst_printing_rule subst x = x -let subst_syntax_extension (subst,(local,sy)) = - (local, List.map (fun (typs,prec,ntn,gr,pp) -> - (typs,prec,ntn,subst_parsing_rule subst gr,subst_printing_rule subst pp)) - sy) +let subst_syntax_extension (subst, (local, sy)) = + let map sy = { sy with + synext_notgram = subst_parsing_rule subst sy.synext_notgram; + synext_unparsing = subst_printing_rule subst sy.synext_unparsing; + } in + (local, List.map map sy) -let classify_syntax_definition (local,_ as o) = +let classify_syntax_definition (local, _ as o) = if local then Dispose else Substitute o -type syntax_extension_obj = - locality_flag * - (notation_var_internalization_type list * Notation.level * - notation * notation_grammar * unparsing list) - list - let inSyntaxExtension : syntax_extension_obj -> obj = declare_object {(default_object "SYNTAX-EXTENSION") with - open_function = (fun i o -> if i=1 then cache_syntax_extension o); + open_function = (fun i o -> if i = 1 then cache_syntax_extension o); cache_function = cache_syntax_extension; subst_function = subst_syntax_extension; classify_function = classify_syntax_definition} @@ -928,7 +952,7 @@ let remove_curly_brackets l = | x :: l -> x :: aux false l in aux true l -let compute_syntax_data (df,modifiers) = +let compute_syntax_data df modifiers = let (assoc,n,etyps,onlyparse,fmt) = interp_modifiers modifiers in let assoc = match assoc with None -> (* default *) Some NonA | a -> a in let toks = split_notation_string df in @@ -958,8 +982,8 @@ let compute_syntax_data (df,modifiers) = (* Return relevant data for interpretation and for parsing/printing *) (msgs,i_data,i_typs,sy_fulldata) -let compute_pure_syntax_data (df,mods) = - let (msgs,(onlyparse,_,_,_),_,sy_data) = compute_syntax_data (df,mods) in +let compute_pure_syntax_data df mods = + let (msgs,(onlyparse,_,_,_),_,sy_data) = compute_syntax_data df mods in let msgs = if onlyparse then (msg_warning, @@ -970,31 +994,38 @@ let compute_pure_syntax_data (df,mods) = (**********************************************************************) (* Registration of notations interpretation *) -let load_notation _ (_,(_,scope,pat,onlyparse,_)) = - Option.iter Notation.declare_scope scope - -let open_notation i (_,(_,scope,pat,onlyparse,(ntn,df))) = - if i=1 & not (Notation.exists_notation_in_scope scope ntn pat) then begin +type notation_obj = { + notobj_local : bool; + notobj_scope : scope_name option; + notobj_interp : interpretation; + notobj_onlyparse : bool; + notobj_notation : notation * notation_location; +} + +let load_notation _ (_, nobj) = + Option.iter Notation.declare_scope nobj.notobj_scope + +let open_notation i (_, nobj) = + let scope = nobj.notobj_scope in + let (ntn, df) = nobj.notobj_notation in + let pat = nobj.notobj_interp in + if i = 1 & not (Notation.exists_notation_in_scope scope ntn pat) then begin (* Declare the interpretation *) Notation.declare_notation_interpretation ntn scope pat df; (* Declare the uninterpretation *) - if not onlyparse then - Notation.declare_uninterpretation (NotationRule (scope,ntn)) pat + if not nobj.notobj_onlyparse then + Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat end let cache_notation o = load_notation 1 o; open_notation 1 o -let subst_notation (subst,(lc,scope,pat,b,ndf)) = - (lc,scope,subst_interpretation subst pat,b,ndf) - -let classify_notation (local,_,_,_,_ as o) = - if local then Dispose else Substitute o +let subst_notation (subst, nobj) = + { nobj with notobj_interp = subst_interpretation subst nobj.notobj_interp; } -type notation_obj = - bool * scope_name option * interpretation * bool * - (notation * notation_location) +let classify_notation nobj = + if nobj.notobj_local then Dispose else Substitute nobj let inNotation : notation_obj -> obj = declare_object {(default_object "NOTATION") with @@ -1038,18 +1069,25 @@ let recover_syntax ntn = try let prec = Notation.level_of_notation ntn in let pp_rule,_ = Notation.find_notation_printing_rule ntn in - let typs,pa_rule = Egramcoq.recover_notation_grammar ntn prec in - (typs,prec,ntn,pa_rule,pp_rule) + let typs, pa_rule = Egramcoq.recover_notation_grammar ntn prec in + { synext_intern = typs; + synext_level = prec; + synext_notation = ntn; + synext_notgram = pa_rule; + synext_unparsing = pp_rule; } with Not_found -> raise NoSyntaxRule -let recover_squash_syntax () = recover_syntax "{ _ }" +let recover_squash_syntax sy = + let sq = recover_syntax "{ _ }" in + [sy; sq] let recover_notation_syntax rawntn = let ntn = contract_notation rawntn in - let (typs,_,_,_,_ as sy_rule) = recover_syntax ntn in - let need_squash = ntn<>rawntn in - typs,if need_squash then [sy_rule; recover_squash_syntax ()] else [sy_rule] + let sy = recover_syntax ntn in + let need_squash = ntn <> rawntn in + let rules = if need_squash then recover_squash_syntax sy else [sy] in + sy.synext_intern, rules (**********************************************************************) (* Main entry point for building parsing and printing rules *) @@ -1057,39 +1095,55 @@ let recover_notation_syntax rawntn = let make_pa_rule (n,typs,symbols,_) ntn = let assoc = recompute_assoc typs in let prod = make_production typs symbols in - (n,assoc,ntn,prod) + { notgram_level = n; + notgram_assoc = assoc; + notgram_notation = ntn; + notgram_prods = prod; } let make_pp_rule (n,typs,symbols,fmt) = match fmt with | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)] - | Some fmt -> hunks_of_format (n,List.split typs) (symbols,parse_format fmt) + | Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt) let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) = let pa_rule = make_pa_rule sy_data ntn in let pp_rule = make_pp_rule sy_data in - let sy_rule = (i_typs,prec,ntn,pa_rule,pp_rule) in + let sy = { + synext_intern = i_typs; + synext_level = prec; + synext_notation = ntn; + synext_notgram = pa_rule; + synext_unparsing = pp_rule; + } in (* By construction, the rule for "{ _ }" is declared, but we need to redeclare it because the file where it is declared needs not be open when the current file opens (especially in presence of -nois) *) - if need_squash then [sy_rule; recover_squash_syntax ()] else [sy_rule] + if need_squash then recover_squash_syntax sy else [sy] (**********************************************************************) (* Main functions about notations *) let add_notation_in_scope local df c mods scope = - let (msgs,i_data,i_typs,sy_data) = compute_syntax_data (df,mods) in + let (msgs,i_data,i_typs,sy_data) = compute_syntax_data df mods in (* Prepare the parsing and printing rules *) let sy_rules = make_syntax_rules sy_data in (* Prepare the interpretation *) - let (onlyparse,recvars,mainvars,df') = i_data in + let (onlyparse, recvars,mainvars, df') = i_data in let i_vars = make_internalization_vars recvars mainvars i_typs in - let (acvars,ac) = interp_notation_constr i_vars recvars c in - let a = (make_interpretation_vars recvars acvars,ac) in - let onlyparse = onlyparse or is_not_printable ac in + let (acvars, ac) = interp_notation_constr i_vars recvars c in + let interp = make_interpretation_vars recvars acvars in + let onlyparse = onlyparse || is_not_printable ac in + let notation = { + notobj_local = local; + notobj_scope = scope; + notobj_interp = (interp, ac); + notobj_onlyparse = onlyparse; + notobj_notation = df'; + } in (* Ready to change the global state *) Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs; - Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)); - Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df')); + Lib.add_anonymous_leaf (inSyntaxExtension (local, sy_rules)); + Lib.add_anonymous_leaf (inNotation notation); df' let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse = @@ -1105,15 +1159,22 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) let df' = (make_notation_key symbs,(path,df)) in let i_vars = make_internalization_vars recvars mainvars i_typs in let (acvars,ac) = interp_notation_constr ~impls i_vars recvars c in - let a = (make_interpretation_vars recvars acvars,ac) in - let onlyparse = onlyparse or is_not_printable ac in - Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df')); + let interp = make_interpretation_vars recvars acvars in + let onlyparse = onlyparse || is_not_printable ac in + let notation = { + notobj_local = local; + notobj_scope = scope; + notobj_interp = (interp, ac); + notobj_onlyparse = onlyparse; + notobj_notation = df'; + } in + Lib.add_anonymous_leaf (inNotation notation); df' (* Notations without interpretation (Reserved Notation) *) let add_syntax_extension local ((loc,df),mods) = - let msgs,sy_data = compute_pure_syntax_data (df,mods) in + let msgs, sy_data = compute_pure_syntax_data df mods in let sy_rules = make_syntax_rules sy_data in Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs; Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) |