From 51efb80ac1699a27e0003349bb766a430fbaf86a Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 29 May 2012 11:09:20 +0000 Subject: Split Egrammar into Egramml and Egramcoq Two gains: - no Summary in Grammar.cma - get rid of the hack concerning error_invalid_pattern_notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15386 85f007b7-540e-0410-9357-904b9bb8a0f7 --- dev/printers.mllib | 3 +- dev/top_printers.ml | 3 +- parsing/argextend.ml4 | 2 +- parsing/egramcoq.ml | 316 +++++++++++++++++++++++++++++++++++++++ parsing/egramcoq.mli | 59 ++++++++ parsing/egrammar.ml | 375 ----------------------------------------------- parsing/egrammar.mli | 77 ---------- parsing/egramml.ml | 67 +++++++++ parsing/egramml.mli | 33 +++++ parsing/grammar.mllib | 6 +- parsing/parsing.mllib | 3 +- parsing/ppvernac.ml | 12 +- parsing/tacextend.ml4 | 8 +- parsing/vernacextend.ml4 | 4 +- toplevel/metasyntax.ml | 9 +- 15 files changed, 500 insertions(+), 477 deletions(-) create mode 100644 parsing/egramcoq.ml create mode 100644 parsing/egramcoq.mli delete mode 100644 parsing/egrammar.ml delete mode 100644 parsing/egrammar.mli create mode 100644 parsing/egramml.ml create mode 100644 parsing/egramml.mli diff --git a/dev/printers.mllib b/dev/printers.mllib index 545a1881fa..928bfc4940 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -139,7 +139,8 @@ Printer Pptactic Ppdecl_proof Tactic_printer -Egrammar +Egramml +Egramcoq Himsg Cerrors Locality diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 4fd6171ac8..2a2833caa5 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -411,7 +411,8 @@ END open Pcoq open Genarg -open Egrammar +open Egramml +open Egramcoq let _ = try diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index b6fd95a815..5a64580d22 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -10,7 +10,7 @@ open Genarg open Q_util -open Egrammar +open Egramml open Pcoq open Compat diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml new file mode 100644 index 0000000000..ee8ec009d7 --- /dev/null +++ b/parsing/egramcoq.ml @@ -0,0 +1,316 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 Topconstr.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' + +(**********************************************************************) +(** 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 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 (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 e -> unfreeze fs; raise e diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli new file mode 100644 index 0000000000..2635195912 --- /dev/null +++ b/parsing/egramcoq.mli @@ -0,0 +1,59 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit + +(** For a declared grammar, returns the rule + the ordered entry types + of variables in the rule (for use in the interpretation) *) +val recover_notation_grammar : + notation -> (precedence * tolerability list) -> + notation_var_internalization_type list * notation_grammar + +val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml deleted file mode 100644 index b0c7054004..0000000000 --- a/parsing/egrammar.ml +++ /dev/null @@ -1,375 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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) - -(* TODO: factorize the error message with error_invalid_pattern_notaition - without introducing useless dependencies *) - -let check_cases_pattern_env loc (env,envlist,hasbinders) = - if hasbinders then - Errors.user_err_loc (loc,"",str "Invalid notation for pattern.") - 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 e -> unfreeze fs; raise e diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli deleted file mode 100644 index 108f39eaab..0000000000 --- a/parsing/egrammar.mli +++ /dev/null @@ -1,77 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit - -val extend_tactic_grammar : - string -> grammar_prod_item list list -> unit - -val extend_vernac_command_grammar : - string -> vernac_expr Gram.entry option -> grammar_prod_item list list -> unit - -val get_extend_vernac_grammars : - unit -> (string * grammar_prod_item list list) list - -(** For a declared grammar, returns the rule + the ordered entry types - of variables in the rule (for use in the interpretation) *) -val recover_notation_grammar : - notation -> (precedence * tolerability list) -> - notation_var_internalization_type list * notation_grammar - -val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b diff --git a/parsing/egramml.ml b/parsing/egramml.ml new file mode 100644 index 0000000000..62e7ae2bbf --- /dev/null +++ b/parsing/egramml.ml @@ -0,0 +1,67 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ('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_gen mkproditem mkact pt = + let (symbs,ntl) = List.split (List.map mkproditem pt) in + let act = make_generic_action mkact 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) + +let make_rule mkact = make_rule_gen make_prod_item mkact + +(** Tactic grammar extensions *) + +let extend_tactic_grammar s gl = + let mkact loc l = Tacexpr.TacExtend (loc,s,List.map snd l) in + let rules = List.map (make_rule mkact) 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 mkact loc l = VernacExtend (s,List.map snd l) in + let rules = List.map (make_rule mkact) gl in + maybe_uncurry (Gram.extend nt) (None,[(None, None, List.rev rules)]) diff --git a/parsing/egramml.mli b/parsing/egramml.mli new file mode 100644 index 0000000000..350e75f90c --- /dev/null +++ b/parsing/egramml.mli @@ -0,0 +1,33 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* grammar_prod_item list list -> unit + +val extend_vernac_command_grammar : + string -> Vernacexpr.vernac_expr Pcoq.Gram.entry option -> + grammar_prod_item list list -> unit + +val get_extend_vernac_grammars : + unit -> (string * grammar_prod_item list list) list + +(** Utility function reused in Egramcoq : *) + +val make_rule : + (Pp.loc -> (Names.identifier * Tacexpr.raw_generic_argument) list -> 'b) -> + grammar_prod_item list -> Pcoq.Gram.symbol list * Pcoq.Gram.action diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib index c99ae47d06..313676c969 100644 --- a/parsing/grammar.mllib +++ b/parsing/grammar.mllib @@ -1,6 +1,5 @@ Coq_config -Profile Pp_control Compat Flags @@ -10,16 +9,13 @@ Unicodetable Errors Util Bigint -Dyn Hashcons Predicate Option Names Libnames -Summary Genarg -Ppextend Tok Lexer Extend @@ -28,7 +24,7 @@ Pcoq Q_util Q_coqast -Egrammar +Egramml Argextend Tacextend Vernacextend diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index 84a08d549a..8414ec7662 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -1,7 +1,8 @@ Extend Extrawit Pcoq -Egrammar +Egramml +Egramcoq G_xml Ppconstr Printer diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index ec164a7e34..1f8d7cb83b 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -77,7 +77,7 @@ let pr_raw_tactic tac = pr_raw_tactic (Global.env()) tac let rec extract_signature = function | [] -> [] - | Egrammar.GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l + | Egramml.GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l | _::l -> extract_signature l let rec match_vernac_rule tys = function @@ -942,19 +942,19 @@ and pr_extend s cl = try pr_gen (Global.env()) a with Failure _ -> str ("") in try - let rls = List.assoc s (Egrammar.get_extend_vernac_grammars()) in + let rls = List.assoc s (Egramml.get_extend_vernac_grammars()) in let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in let start,rl,cl = match rl with - | Egrammar.GramTerminal s :: rl -> str s, rl, cl - | Egrammar.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl + | Egramml.GramTerminal s :: rl -> str s, rl, cl + | Egramml.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl | [] -> anomaly "Empty entry" in let (pp,_) = List.fold_left (fun (strm,args) pi -> let pp,args = match pi with - | Egrammar.GramNonTerminal _ -> (pr_arg (List.hd args), List.tl args) - | Egrammar.GramTerminal s -> (str s, args) in + | Egramml.GramNonTerminal _ -> (pr_arg (List.hd args), List.tl args) + | Egramml.GramTerminal s -> (str s, args) in (strm ++ spc() ++ pp), args) (start,cl) rl in hov 1 pp diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index c7a646ac49..ec0784c529 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -16,7 +16,7 @@ open Q_coqast open Argextend open Pcoq open Extrawit -open Egrammar +open Egramml open Compat let rec make_patt = function @@ -95,9 +95,9 @@ let mlexpr_terminals_of_grammar_tactic_prod_item_expr = function | GramNonTerminal (loc,nt,_,sopt) -> <:expr< None >> let make_prod_item = function - | GramTerminal s -> <:expr< Egrammar.GramTerminal $str:s$ >> + | GramTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> | GramNonTerminal (loc,nt,g,sopt) -> - <:expr< Egrammar.GramNonTerminal $default_loc$ $mlexpr_of_argtype loc nt$ + <:expr< Egramml.GramNonTerminal $default_loc$ $mlexpr_of_argtype loc nt$ $mlexpr_of_prod_entry_key g$ $mlexpr_of_option mlexpr_of_ident sopt$ >> let mlexpr_of_clause = @@ -190,7 +190,7 @@ let declare_tactic loc s cl = | None -> () ]) $atomic_tactics$ with e -> Pp.pp (Errors.print e); - Egrammar.extend_tactic_grammar $se$ $gl$; + Egramml.extend_tactic_grammar $se$ $gl$; List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >> ]) diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 7553aef4a7..94135d1211 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -16,7 +16,7 @@ open Q_coqast open Argextend open Tacextend open Pcoq -open Egrammar +open Egramml open Compat let rec make_let e = function @@ -56,7 +56,7 @@ let declare_command loc s nt cl = [ <:str_item< do { try Vernacinterp.vinterp_add $mlexpr_of_string s$ $funcl$ with e -> Pp.pp (Errors.print e); - Egrammar.extend_vernac_command_grammar $mlexpr_of_string s$ $nt$ $gl$ + Egramml.extend_vernac_command_grammar $mlexpr_of_string s$ $nt$ $gl$ } >> ] open Pcaml diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 203d8ba022..e98aa8c260 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -27,7 +27,8 @@ open Glob_term open Libnames open Tok open Lexer -open Egrammar +open Egramml +open Egramcoq open Notation open Nameops @@ -65,7 +66,7 @@ let rec make_tags = function | [] -> [] let cache_tactic_notation (_,(pa,pp)) = - Egrammar.extend_grammar (Egrammar.TacticGrammar pa); + Egramcoq.extend_grammar (Egramcoq.TacticGrammar pa); Pptactic.declare_extra_tactic_pprule pp let subst_tactic_parule subst (key,n,p,(d,tac)) = @@ -700,7 +701,7 @@ let cache_one_syntax_extension (typs,prec,ntn,gr,pp) = (* Reserve the notation level *) Notation.declare_notation_level ntn prec; (* Declare the parsing rule *) - Egrammar.extend_grammar (Egrammar.Notation (prec,typs,gr)); + Egramcoq.extend_grammar (Egramcoq.Notation (prec,typs,gr)); (* Declare the printing rule *) Notation.declare_notation_printing_rule ntn (pp,fst prec) @@ -1023,7 +1024,7 @@ 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 = Egrammar.recover_notation_grammar ntn prec in + let typs,pa_rule = Egramcoq.recover_notation_grammar ntn prec in (typs,prec,ntn,pa_rule,pp_rule) with Not_found -> raise NoSyntaxRule -- cgit v1.2.3