diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/extend.ml | 3 | ||||
| -rw-r--r-- | parsing/g_constr.mlg | 6 | ||||
| -rw-r--r-- | parsing/notation_gram.ml | 12 | ||||
| -rw-r--r-- | parsing/notgram_ops.ml | 37 | ||||
| -rw-r--r-- | parsing/notgram_ops.mli | 9 | ||||
| -rw-r--r-- | parsing/parsing.mllib | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 52 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 5 | ||||
| -rw-r--r-- | parsing/ppextend.ml | 83 | ||||
| -rw-r--r-- | parsing/ppextend.mli | 28 |
10 files changed, 143 insertions, 94 deletions
diff --git a/parsing/extend.ml b/parsing/extend.ml index dcdaa25c33..848861238a 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -21,6 +21,7 @@ type production_position = type production_level = | NextLevel | NumLevel of int + | DefaultLevel (** Interpreted differently at the border or inside a rule *) (** User-level types used to tell how to parse or interpret of the non-terminal *) @@ -40,7 +41,7 @@ type constr_entry_key = (** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *) type simple_constr_prod_entry_key = - production_level option constr_entry_key_gen + production_level constr_entry_key_gen (** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *) diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index dcc3a87b11..d6c6c365cb 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -199,11 +199,11 @@ GRAMMAR EXTEND Gram collapse -(3) into the numeral -3. *) (match c.CAst.v with | CPrim (Numeral (SPlus,n)) -> - CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"( _ )"),([c],[],[],[])) + CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"( _ )"),([c],[],[],[])) | _ -> c) } | "{|"; c = record_declaration; bar_cbrace -> { c } | "{"; c = binder_constr ; "}" -> - { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) } + { CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) } | "`{"; c = operconstr LEVEL "200"; "}" -> { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) } | "`("; c = operconstr LEVEL "200"; ")" -> @@ -380,7 +380,7 @@ GRAMMAR EXTEND Gram collapse -(3) into the numeral -3. *) match p.CAst.v with | CPatPrim (Numeral (SPlus,n)) -> - CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[]) + CAst.make ~loc @@ CPatNotation(None,(InConstrEntrySomeLevel,"( _ )"),([p],[]),[]) | _ -> p } | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" -> { CAst.make ~loc @@ CPatOr (p::pl) } diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml index 9f133ca9d4..427505c199 100644 --- a/parsing/notation_gram.ml +++ b/parsing/notation_gram.ml @@ -10,14 +10,11 @@ open Names open Extend +open Constrexpr (** Dealing with precedences *) -type precedence = int -type parenRelation = L | E | Any | Prec of precedence -type tolerability = precedence * parenRelation - -type level = Constrexpr.notation_entry * precedence * tolerability list * constr_entry_key list +type level = notation_entry * entry_level * entry_relative_level list * constr_entry_key list (* first argument is InCustomEntry s for custom entries *) type grammar_constr_prod_item = @@ -37,7 +34,4 @@ type one_notation_grammar = { notgram_prods : grammar_constr_prod_item list list; } -type notation_grammar = { - notgram_onlyprinting : bool; - notgram_rules : one_notation_grammar list -} +type notation_grammar = one_notation_grammar list diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml index 009dafdb13..b6699493bb 100644 --- a/parsing/notgram_ops.ml +++ b/parsing/notgram_ops.ml @@ -12,33 +12,36 @@ open Pp open CErrors open Util open Notation -open Notation_gram +open Constrexpr -(* Uninterpreted notation levels *) +(* Register the level of notation for parsing and printing + (also register the parsing rule if not onlyprinting) *) let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty -let declare_notation_level ?(onlyprint=false) ntn level = +let declare_notation_level ntn parsing_rule level = try - let (level,onlyprint) = NotationMap.find ntn !notation_level_map in - if not onlyprint then anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.") + let _ = NotationMap.find ntn !notation_level_map in + anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.") with Not_found -> - notation_level_map := NotationMap.add ntn (level,onlyprint) !notation_level_map + notation_level_map := NotationMap.add ntn (parsing_rule,level) !notation_level_map -let level_of_notation ?(onlyprint=false) ntn = - let (level,onlyprint') = NotationMap.find ntn !notation_level_map in - if onlyprint' && not onlyprint then raise Not_found; - level +let level_of_notation ntn = + NotationMap.find ntn !notation_level_map + +let get_defined_notations () = + NotationSet.elements @@ NotationMap.domain !notation_level_map (**********************************************************************) (* Equality *) open Extend -let parenRelation_eq t1 t2 = match t1, t2 with -| L, L | E, E | Any, Any -> true -| Prec l1, Prec l2 -> Int.equal l1 l2 -| _ -> false +let entry_relative_level_eq t1 t2 = match t1, t2 with +| LevelLt n1, LevelLt n2 -> Int.equal n1 n2 +| LevelLe n1, LevelLe n2 -> Int.equal n1 n2 +| LevelSome, LevelSome -> true +| (LevelLt _ | LevelLe _ | LevelSome), _ -> false let production_position_eq pp1 pp2 = match (pp1,pp2) with | BorderProd (side1,assoc1), BorderProd (side2,assoc2) -> side1 = side2 && assoc1 = assoc2 @@ -48,7 +51,8 @@ let production_position_eq pp1 pp2 = match (pp1,pp2) with let production_level_eq l1 l2 = match (l1,l2) with | NextLevel, NextLevel -> true | NumLevel n1, NumLevel n2 -> Int.equal n1 n2 -| (NextLevel | NumLevel _), _ -> false +| DefaultLevel, DefaultLevel -> true +| (NextLevel | NumLevel _ | DefaultLevel), _ -> false let constr_entry_key_eq eq v1 v2 = match v1, v2 with | ETIdent, ETIdent -> true @@ -61,11 +65,10 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with | (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) = - let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in let prod_eq (l1,pp1) (l2,pp2) = not strict || (production_level_eq l1 l2 && production_position_eq pp1 pp2) in - notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal tolerability_eq t1 t2 + notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal entry_relative_level_eq t1 t2 && List.equal (constr_entry_key_eq prod_eq) u1 u2 let level_eq = level_eq_gen false diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli index c31f4505e7..d8b7e8e4c1 100644 --- a/parsing/notgram_ops.mli +++ b/parsing/notgram_ops.mli @@ -13,8 +13,13 @@ open Constrexpr open Notation_gram val level_eq : level -> level -> bool +val entry_relative_level_eq : entry_relative_level -> entry_relative_level -> bool (** {6 Declare and test the level of a (possibly uninterpreted) notation } *) -val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit -val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *) +val declare_notation_level : notation -> notation_grammar option -> level -> unit +val level_of_notation : notation -> notation_grammar option * level + (** raise [Not_found] if not declared *) + +(** Returns notations with defined parsing/printing rules *) +val get_defined_notations : unit -> notation list diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index 2154f2f881..12311f9cd9 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -2,8 +2,8 @@ Tok CLexer Extend Notation_gram -Ppextend Notgram_ops +Ppextend Pcoq G_constr G_prim diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 26afdcb9d5..92c3b7c6e8 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -212,7 +212,8 @@ type 'a extend_statement = 'a single_extend_statement list type extend_rule = -| ExtendRule : 'a G.Entry.e * gram_reinit option * 'a extend_statement -> extend_rule +| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule +| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule module EntryCommand = Dyn.Make () module EntryData = struct type _ t = Ex : 'b G.Entry.e String.Map.t -> ('a * 'b) t end @@ -231,33 +232,39 @@ let camlp5_entries = ref EntryDataMap.empty (** Deletion *) -let grammar_delete e reinit (pos,rls) = +let grammar_delete e (pos,rls) = List.iter (fun (n,ass,lev) -> List.iter (fun (AnyProduction (pil,_)) -> G.safe_delete_rule e pil) (List.rev lev)) - (List.rev rls); - match reinit with - | Some (a,ext) -> - let lev = match pos with + (List.rev rls) + +let grammar_delete_reinit e reinit (pos, rls) = + grammar_delete e (pos, rls); + let a, ext = reinit in + let lev = match pos with | Some (Gramext.Level n) -> n | _ -> assert false - in - let warning msg = Feedback.msg_warning Pp.(str msg) in - (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]] - | None -> () + in + let warning msg = Feedback.msg_warning Pp.(str msg) in + (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]] (** Extension *) -let grammar_extend e reinit ext = +let grammar_extend e ext = let ext = of_coq_extend_statement ext in - let undo () = grammar_delete e reinit ext in + let undo () = grammar_delete e ext in let pos, ext = fix_extend_statement ext in let redo () = G.safe_extend ~warning:None e pos ext in camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state; redo () -let grammar_extend_sync e reinit ext = - camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state; +let grammar_extend_sync e ext = + camlp5_state := ByGrammar (ExtendRule (e, ext)) :: !camlp5_state; + let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in + G.safe_extend ~warning:None e pos ext + +let grammar_extend_sync_reinit e reinit ext = + camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state; let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in G.safe_extend ~warning:None e pos ext @@ -278,8 +285,12 @@ let rec remove_grammars n = if n>0 then match !camlp5_state with | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove.") - | ByGrammar (ExtendRule (g, reinit, ext)) :: t -> - grammar_delete g reinit (of_coq_extend_statement ext); + | ByGrammar (ExtendRuleReinit (g, reinit, ext)) :: t -> + grammar_delete_reinit g reinit (of_coq_extend_statement ext); + camlp5_state := t; + remove_grammars (n-1) + | ByGrammar (ExtendRule (g, ext)) :: t -> + grammar_delete g (of_coq_extend_statement ext); camlp5_state := t; remove_grammars (n-1) | ByEXTEND (undo,redo)::t -> @@ -507,6 +518,12 @@ let create_entry_command name (interp : ('a, 'b) entry_extension) : ('a, 'b) ent let () = entry_interp := EntryInterpMap.add obj (EntryInterp.Ex interp) !entry_interp in obj +let iter_extend_sync = function + | ExtendRule (e, ext) -> + grammar_extend_sync e ext + | ExtendRuleReinit (e, reinit, ext) -> + grammar_extend_sync_reinit e reinit ext + let extend_grammar_command tag g = let modify = GrammarInterpMap.find tag !grammar_interp in let grammar_state = match !grammar_stack with @@ -514,8 +531,7 @@ let extend_grammar_command tag g = | (_, 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 () = List.iter iter_extend_sync rules in let nb = List.length rules in grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 404fbdb4fd..f2fc007a7b 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -225,7 +225,7 @@ type 'a extend_statement = Gramlib.Gramext.position option * 'a single_extend_statement list -val grammar_extend : 'a Entry.t -> gram_reinit option -> 'a extend_statement -> unit +val grammar_extend : 'a Entry.t -> 'a extend_statement -> unit (** Extend the grammar of Coq, without synchronizing it with the backtracking mechanism. This means that grammar extensions defined this way will survive an undo. *) @@ -242,7 +242,8 @@ type 'a grammar_command marshallable. *) type extend_rule = -| ExtendRule : 'a Entry.t * gram_reinit option * 'a extend_statement -> extend_rule +| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule +| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t (** Grammar extension entry point. Given some ['a] and a current grammar state, diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml index 7368f4109e..bb6693a239 100644 --- a/parsing/ppextend.ml +++ b/parsing/ppextend.ml @@ -12,7 +12,8 @@ open Util open Pp open CErrors open Notation -open Notation_gram +open Constrexpr +open Notgram_ops (*s Pretty-print. *) @@ -37,41 +38,67 @@ let ppcmd_of_cut = function | PpBrk(n1,n2) -> brk(n1,n2) type unparsing = - | UnpMetaVar of int * parenRelation - | UnpBinderMetaVar of int * parenRelation - | UnpListMetaVar of int * parenRelation * unparsing list - | UnpBinderListMetaVar of int * bool * unparsing list + | UnpMetaVar of entry_relative_level * Extend.side option + | UnpBinderMetaVar of entry_relative_level + | UnpListMetaVar of entry_relative_level * unparsing list * Extend.side option + | UnpBinderListMetaVar of bool * unparsing list | UnpTerminal of string | UnpBox of ppbox * unparsing Loc.located list | UnpCut of ppcut -type unparsing_rule = unparsing list * precedence +type unparsing_rule = unparsing list * entry_level type extra_unparsing_rules = (string * string) list -(* Concrete syntax for symbolic-extension table *) -let notation_rules = - Summary.ref ~name:"notation-rules" (NotationMap.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) NotationMap.t) - -let declare_notation_rule ntn ~extra unpl gram = - notation_rules := NotationMap.add ntn (unpl,extra,gram) !notation_rules - -let find_notation_printing_rule ntn = - try pi1 (NotationMap.find ntn !notation_rules) - with Not_found -> anomaly (str "No printing rule found for " ++ pr_notation ntn ++ str ".") -let find_notation_extra_printing_rules ntn = - try pi2 (NotationMap.find ntn !notation_rules) - with Not_found -> [] -let find_notation_parsing_rules ntn = - try pi3 (NotationMap.find ntn !notation_rules) - with Not_found -> anomaly (str "No parsing rule found for " ++ pr_notation ntn ++ str ".") - -let get_defined_notations () = - NotationSet.elements @@ NotationMap.domain !notation_rules + +let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with + | UnpMetaVar (p1,s1), UnpMetaVar (p2,s2) -> entry_relative_level_eq p1 p2 && s1 = s2 + | UnpBinderMetaVar p1, UnpBinderMetaVar p2 -> entry_relative_level_eq p1 p2 + | UnpListMetaVar (p1,l1,s1), UnpListMetaVar (p2,l2,s2) -> entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2 && s1 = s2 + | UnpBinderListMetaVar (b1,l1), UnpBinderListMetaVar (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq l1 l2 + | UnpTerminal s1, UnpTerminal s2 -> String.equal s1 s2 + | UnpBox (b1,l1), UnpBox (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq (List.map snd l1) (List.map snd l2) + | UnpCut p1, UnpCut p2 -> p1 = p2 + | (UnpMetaVar _ | UnpBinderMetaVar _ | UnpListMetaVar _ | + UnpBinderListMetaVar _ | UnpTerminal _ | UnpBox _ | UnpCut _), _ -> false + +(* Register generic and specific printing rules *) + +let generic_notation_printing_rules = + Summary.ref ~name:"generic-notation-printing-rules" (NotationMap.empty : (unparsing_rule * bool * extra_unparsing_rules) NotationMap.t) + +let specific_notation_printing_rules = + Summary.ref ~name:"specific-notation-printing-rules" (SpecificNotationMap.empty : (unparsing_rule * extra_unparsing_rules) SpecificNotationMap.t) + +let declare_generic_notation_printing_rules ntn ~reserved ~extra unpl = + generic_notation_printing_rules := NotationMap.add ntn (unpl,reserved,extra) !generic_notation_printing_rules +let declare_specific_notation_printing_rules specific_ntn ~extra unpl = + specific_notation_printing_rules := SpecificNotationMap.add specific_ntn (unpl,extra) !specific_notation_printing_rules + +let has_generic_notation_printing_rule ntn = + NotationMap.mem ntn !generic_notation_printing_rules + +let find_generic_notation_printing_rule ntn = + NotationMap.find ntn !generic_notation_printing_rules + +let find_specific_notation_printing_rule specific_ntn = + SpecificNotationMap.find specific_ntn !specific_notation_printing_rules + +let find_notation_printing_rule which ntn = + try match which with + | None -> raise Not_found (* Normally not the case *) + | Some which -> fst (find_specific_notation_printing_rule (which,ntn)) + with Not_found -> pi1 (find_generic_notation_printing_rule ntn) + +let find_notation_extra_printing_rules which ntn = + try match which with + | None -> raise Not_found + | Some which -> snd (find_specific_notation_printing_rule (which,ntn)) + with Not_found -> pi3 (find_generic_notation_printing_rule ntn) let add_notation_extra_printing_rule ntn k v = try - notation_rules := - let p, pp, gr = NotationMap.find ntn !notation_rules in - NotationMap.add ntn (p, (k,v) :: pp, gr) !notation_rules + generic_notation_printing_rules := + let p, b, pp = NotationMap.find ntn !generic_notation_printing_rules in + NotationMap.add ntn (p, b, (k,v) :: pp) !generic_notation_printing_rules with Not_found -> user_err ~hdr:"add_notation_extra_printing_rule" (str "No such Notation.") diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli index be5af75e72..18e48942c6 100644 --- a/parsing/ppextend.mli +++ b/parsing/ppextend.mli @@ -9,7 +9,6 @@ (************************************************************************) open Constrexpr -open Notation_gram (** {6 Pretty-print. } *) @@ -31,21 +30,24 @@ val ppcmd_of_cut : ppcut -> Pp.t (** Declare and look for the printing rule for symbolic notations *) type unparsing = - | UnpMetaVar of int * parenRelation - | UnpBinderMetaVar of int * parenRelation - | UnpListMetaVar of int * parenRelation * unparsing list - | UnpBinderListMetaVar of int * bool * unparsing list + | UnpMetaVar of entry_relative_level * Extend.side option + | UnpBinderMetaVar of entry_relative_level + | UnpListMetaVar of entry_relative_level * unparsing list * Extend.side option + | UnpBinderListMetaVar of bool * unparsing list | UnpTerminal of string | UnpBox of ppbox * unparsing Loc.located list | UnpCut of ppcut -type unparsing_rule = unparsing list * precedence +type unparsing_rule = unparsing list * entry_level type extra_unparsing_rules = (string * string) list -val declare_notation_rule : notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit -val find_notation_printing_rule : notation -> unparsing_rule -val find_notation_extra_printing_rules : notation -> extra_unparsing_rules -val find_notation_parsing_rules : notation -> notation_grammar -val add_notation_extra_printing_rule : notation -> string -> string -> unit -(** Returns notations with defined parsing/printing rules *) -val get_defined_notations : unit -> notation list +val unparsing_eq : unparsing -> unparsing -> bool + +val declare_generic_notation_printing_rules : notation -> reserved:bool -> extra:extra_unparsing_rules -> unparsing_rule -> unit +val declare_specific_notation_printing_rules : specific_notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit +val has_generic_notation_printing_rule : notation -> bool +val find_generic_notation_printing_rule : notation -> unparsing_rule * bool * extra_unparsing_rules +val find_specific_notation_printing_rule : specific_notation -> unparsing_rule * extra_unparsing_rules +val find_notation_printing_rule : notation_with_optional_scope option -> notation -> unparsing_rule +val find_notation_extra_printing_rules : notation_with_optional_scope option -> notation -> extra_unparsing_rules +val add_notation_extra_printing_rule : notation -> string -> string -> unit |