diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/extend.ml | 1 | ||||
| -rw-r--r-- | parsing/extend.mli | 1 | ||||
| -rw-r--r-- | parsing/g_constr.mlg | 20 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 2 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 | ||||
| -rw-r--r-- | parsing/ppextend.ml | 6 | ||||
| -rw-r--r-- | parsing/ppextend.mli | 4 |
7 files changed, 32 insertions, 4 deletions
diff --git a/parsing/extend.ml b/parsing/extend.ml index a6fa6edad5..94c3768116 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -58,6 +58,7 @@ type constr_prod_entry_key = | ETProdName (* Parsed as a name (ident or _) *) | ETProdReference (* Parsed as a global reference *) | ETProdBigint (* Parsed as an (unbounded) integer *) + | ETProdOneBinder of bool (* Parsed as name, or name:type or 'pattern, possibly in closed form *) | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *) | ETProdPattern of int (* Parsed as pattern as a binder (as subpart of a constr) *) | ETProdConstrList of Constrexpr.notation_entry * (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr, or subentries of those *) diff --git a/parsing/extend.mli b/parsing/extend.mli index 057fdb3841..b698415fd6 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -53,6 +53,7 @@ type constr_prod_entry_key = | ETProdName (* Parsed as a name (ident or _) *) | ETProdReference (* Parsed as a global reference *) | ETProdBigint (* Parsed as an (unbounded) integer *) + | ETProdOneBinder of bool (* Parsed as name, or name:type or 'pattern, possibly in closed form *) | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *) | ETProdPattern of int (* Parsed as pattern as a binder (as subpart of a constr) *) | ETProdConstrList of Constrexpr.notation_entry * (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr, or subentries of those *) diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 67a061175a..9b4b41acd2 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -39,6 +39,10 @@ let binder_of_name expl { CAst.loc = loc; v = na } = let binders_of_names l = List.map (binder_of_name Explicit) l +let pat_of_name CAst.{loc;v} = match v with +| Anonymous -> CAst.make ?loc @@ CPatAtom None +| Name id -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident id)) + let err () = raise Stream.Failure (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) @@ -84,7 +88,8 @@ GRAMMAR EXTEND Gram universe_level universe_name sort sort_family global constr_pattern cpattern Constr.ident closed_binder open_binders binder binders binders_fixannot - record_declaration typeclass_constraint pattern arg type_cstr; + record_declaration typeclass_constraint pattern arg type_cstr + one_closed_binder one_open_binder; Constr.ident: [ [ id = Prim.ident -> { id } ] ] ; @@ -446,6 +451,19 @@ GRAMMAR EXTEND Gram in [CLocalPattern (CAst.make ~loc (p, ty))] } ] ] ; + one_open_binder: + [ [ na = name -> { (pat_of_name na, Explicit) } + | na = name; ":"; t = lconstr -> { (CAst.make ~loc @@ CPatCast (pat_of_name na, t), Explicit) } + | b = one_closed_binder -> { b } ] ] + ; + one_closed_binder: + [ [ "("; na = name; ":"; t = lconstr; ")" -> { (CAst.make ~loc @@ CPatCast (pat_of_name na, t), Explicit) } + | "{"; na = name; "}" -> { (pat_of_name na, MaxImplicit) } + | "{"; na = name; ":"; t = lconstr; "}" -> { (CAst.make ~loc @@ CPatCast (pat_of_name na, t), MaxImplicit) } + | "["; na = name; "]" -> { (pat_of_name na, NonMaxImplicit) } + | "["; na = name; ":"; t = lconstr; "]" -> { (CAst.make ~loc @@ CPatCast (pat_of_name na, t), NonMaxImplicit) } + | "'"; p = pattern LEVEL "0" -> { (p, Explicit) } ] ] + ; typeclass_constraint: [ [ "!" ; c = term LEVEL "200" -> { (CAst.make ~loc Anonymous), true, c } | "{"; id = name; "}"; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = term LEVEL "200" -> diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 22b5e70311..d49a49d242 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -327,6 +327,8 @@ module Constr = let binder = Entry.create "binder" let binders = Entry.create "binders" let open_binders = Entry.create "open_binders" + let one_open_binder = Entry.create "one_open_binder" + let one_closed_binder = Entry.create "one_closed_binder" let binders_fixannot = Entry.create "binders_fixannot" let typeclass_constraint = Entry.create "typeclass_constraint" let record_declaration = Entry.create "record_declaration" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index ce4c91d51f..d0ae594db1 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -203,6 +203,8 @@ module Constr : val binder : local_binder_expr list Entry.t (* closed_binder or variable *) val binders : local_binder_expr list Entry.t (* list of binder *) val open_binders : local_binder_expr list Entry.t + val one_open_binder : kinded_cases_pattern_expr Entry.t + val one_closed_binder : kinded_cases_pattern_expr Entry.t val binders_fixannot : (local_binder_expr list * recursion_order_expr option) Entry.t val typeclass_constraint : (lname * bool * constr_expr) Entry.t val record_declaration : constr_expr Entry.t diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml index aab385a707..b64c2b956a 100644 --- a/parsing/ppextend.ml +++ b/parsing/ppextend.ml @@ -36,9 +36,11 @@ let ppcmd_of_cut = function | PpFnl -> fnl () | PpBrk(n1,n2) -> brk(n1,n2) +type pattern_quote_style = QuotedPattern | NotQuotedPattern + type unparsing = | UnpMetaVar of entry_relative_level * Extend.side option - | UnpBinderMetaVar of entry_relative_level + | UnpBinderMetaVar of entry_relative_level * pattern_quote_style | UnpListMetaVar of entry_relative_level * unparsing list * Extend.side option | UnpBinderListMetaVar of bool * unparsing list | UnpTerminal of string @@ -50,7 +52,7 @@ type extra_unparsing_rules = (string * string) list 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 + | UnpBinderMetaVar (p1,s1), UnpBinderMetaVar (p2,s2) -> entry_relative_level_eq p1 p2 && s1 = s2 | 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 diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli index 56a3fc8e3c..ca22aacacf 100644 --- a/parsing/ppextend.mli +++ b/parsing/ppextend.mli @@ -28,10 +28,12 @@ val ppcmd_of_cut : ppcut -> Pp.t (** {6 Printing rules for notations} *) +type pattern_quote_style = QuotedPattern | NotQuotedPattern + (** Declare and look for the printing rule for symbolic notations *) type unparsing = | UnpMetaVar of entry_relative_level * Extend.side option - | UnpBinderMetaVar of entry_relative_level + | UnpBinderMetaVar of entry_relative_level * pattern_quote_style | UnpListMetaVar of entry_relative_level * unparsing list * Extend.side option | UnpBinderListMetaVar of bool * unparsing list | UnpTerminal of string |