diff options
| -rw-r--r-- | intf/extend.ml | 29 | ||||
| -rw-r--r-- | parsing/egramcoq.ml | 23 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 1 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 27 |
4 files changed, 44 insertions, 36 deletions
diff --git a/intf/extend.ml b/intf/extend.ml index e4d014a09..79bbbd376 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -29,32 +29,41 @@ type production_level = | NextLevel | NumLevel of int -type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list +(** User-level types used to tell how to parse or interpret of the non-terminal *) type ('lev,'pos) constr_entry_key_gen = - | ETName | ETReference | ETBigint - | ETBinder of bool + | ETName + | ETReference + | ETBigint + | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) | ETConstr of ('lev * 'pos) | ETPattern | ETOther of string * string - | ETConstrList of ('lev * 'pos) * Tok.t list - | ETBinderList of binder_entry_kind (** Entries level (left-hand-side of grammar rules) *) type constr_entry_key = (int,unit) constr_entry_key_gen -(** Entries used in productions (in right-hand-side of grammar rules) *) - -type constr_prod_entry_key = - (production_level,production_position) constr_entry_key_gen - (** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *) type simple_constr_prod_entry_key = (production_level,unit) constr_entry_key_gen +(** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *) + +type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list + +type constr_prod_entry_key = + | ETProdName (* Parsed as a name (ident or _) *) + | ETProdReference (* Parsed as a global reference *) + | ETProdBigint (* Parsed as an (unbounded) integer *) + | ETProdConstr of (production_level * production_position) (* Parsed as constr or pattern *) + | ETProdPattern (* Parsed as pattern (as subpart of a constr) *) + | ETProdOther of string * string (* Intended for embedding custom entries in constr or pattern *) + | ETProdConstrList of (production_level * production_position) * Tok.t list (* Parsed as non-empty list of constr *) + | ETProdBinderList of binder_entry_kind (* Parsed as non-empty list of local binders *) + (** {5 AST for user-provided entries} *) type 'a user_symbol = diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 16124c26c..3c4f408f8 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -229,7 +229,6 @@ type (_, _) entry = | TTName : ('self, Name.t Loc.located) entry | TTReference : ('self, reference) entry | TTBigint : ('self, Constrexpr.raw_natural_number) entry -| TTBinder : ('self, local_binder_expr list) entry | TTConstr : prod_info * 'r target -> ('r, 'r) entry | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry | TTOpenBinderList : ('self, local_binder_expr list) entry @@ -292,23 +291,20 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun as | TTClosedBinderList [] -> Alist1 (Aentry Constr.binder) | TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl) | TTName -> Aentry Prim.name -| TTBinder -> Aentry Constr.binder | TTOpenBinderList -> Aentry Constr.open_binders | TTBigint -> Aentry Prim.bigint | TTReference -> Aentry Constr.global let interp_entry forpat e = match e with -| ETName -> TTAny TTName -| ETReference -> TTAny TTReference -| ETBigint -> TTAny TTBigint -| ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList.") -| ETBinder false -> TTAny TTBinder -| ETConstr p -> TTAny (TTConstr (p, forpat)) -| ETPattern -> assert false (** not used *) -| ETOther _ -> assert false (** not used *) -| ETConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat)) -| ETBinderList ETBinderOpen -> TTAny TTOpenBinderList -| ETBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl) +| ETProdName -> TTAny TTName +| ETProdReference -> TTAny TTReference +| ETProdBigint -> TTAny TTBigint +| ETProdConstr p -> TTAny (TTConstr (p, forpat)) +| ETProdPattern -> assert false (** not used *) +| ETProdOther _ -> assert false (** not used *) +| ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat)) +| ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList +| ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl) let constr_expr_of_name (loc,na) = CAst.make ?loc @@ match na with | Anonymous -> CHole (None,Misctypes.IntroAnonymous,None) @@ -334,7 +330,6 @@ match e with | ForConstr -> push_constr subst (constr_expr_of_name v) | ForPattern -> push_constr subst (cases_pattern_expr_of_name v) end -| TTBinder -> { subst with binders = (v, true) :: subst.binders } | TTOpenBinderList -> { subst with binders = (v, true) :: subst.binders } | TTClosedBinderList _ -> { subst with binders = (List.flatten v, false) :: subst.binders } | TTBigint -> diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 950246c53..a7e73c91f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -102,7 +102,6 @@ open Decl_kinds | ETBigint -> str "bigint" | ETBinder true -> str "binder" | ETBinder false -> str "closed binder" - | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type" let pr_comment pr_c = function | CommentConstr c -> pr_c c diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index bb4db1322..09eb0503d 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -574,8 +574,8 @@ let hunks_of_format (from,(vars,typs)) symfmt = let assoc_of_type n (_,typ) = precedence_of_entry_type n typ let is_not_small_constr = function - ETConstr _ -> true - | ETOther("constr","binder_constr") -> true + ETProdConstr _ -> true + | ETProdOther("constr","binder_constr") -> true | _ -> false let rec define_keywords_aux = function @@ -607,14 +607,14 @@ let distribute a ll = List.map (fun l -> a @ l) ll let expand_list_rule typ tkl x n p ll = let camlp5_message_name = Some (add_suffix x ("_"^string_of_int n)) in - let main = GramConstrNonTerminal (ETConstr typ, camlp5_message_name) in + let main = GramConstrNonTerminal (ETProdConstr typ, camlp5_message_name) in let tks = List.map (fun x -> GramConstrTerminal x) tkl in let rec aux i hds ll = if i < p then aux (i+1) (main :: tks @ hds) ll else if Int.equal i (p+n) then let hds = GramConstrListMark (p+n,true,p) :: hds - @ [GramConstrNonTerminal (ETConstrList (typ,tkl), Some x)] in + @ [GramConstrNonTerminal (ETProdConstrList (typ,tkl), Some x)] in distribute hds ll else distribute (GramConstrListMark (i+1,false,p) :: hds @ [main]) ll @ @@ -636,12 +636,21 @@ let include_possible_similar_trailing_pattern typ etyps sl l = with Exit -> n,l in try_aux 0 l +let prod_entry_type = function + | ETName -> ETProdName + | ETReference -> ETProdReference + | ETBigint -> ETProdBigint + | ETBinder _ -> assert false (* See check_binder_type *) + | ETConstr p -> ETProdConstr p + | ETPattern -> ETProdPattern + | ETOther (s,t) -> ETProdOther (s,t) + let make_production etyps symbols = let rec aux = function | [] -> [[]] | NonTerminal m :: l -> let typ = List.assoc m etyps in - distribute [GramConstrNonTerminal (typ, Some m)] (aux l) + distribute [GramConstrNonTerminal (prod_entry_type typ, Some m)] (aux l) | Terminal s :: l -> distribute [GramConstrTerminal (CLexer.terminal s)] (aux l) | Break _ :: l -> @@ -658,8 +667,8 @@ let make_production etyps symbols = | ETBinder o -> check_open_binder o sl x; let typ = if o then (assert (tkl = []); ETBinderOpen) else ETBinderClosed tkl in - distribute - [GramConstrNonTerminal (ETBinderList typ, Some x)] (aux l) + distribute + [GramConstrNonTerminal (ETProdBinderList typ, Some x)] (aux l) | _ -> user_err Pp.(str "Components of recursive patterns in notation must be terms or binders.") in let prods = aux symbols in @@ -909,7 +918,6 @@ let set_entry_type etyps (x,typ) = | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd) | (ETPattern | ETName | ETBigint | ETOther _ | ETReference | ETBinder _ as t), _ -> t - | (ETBinderList _ |ETConstrList _), _ -> assert false with Not_found -> ETConstr typ in (x,typ) @@ -934,7 +942,6 @@ let internalization_type_of_entry_type = function | ETBinder _ -> NtnInternTypeBinder | ETName -> NtnInternTypeIdent | ETPattern | ETOther _ -> user_err Pp.(str "Not supported.") - | ETBinderList _ | ETConstrList _ -> assert false let set_internalization_type typs = List.map (fun (_, e) -> internalization_type_of_entry_type e) typs @@ -1039,8 +1046,6 @@ let find_precedence lev etyps symbols onlyprint = if Option.is_empty lev then user_err Pp.(str "Need an explicit level.") else [],Option.get lev - | ETConstrList _ | ETBinderList _ -> - assert false (* internally used in grammar only *) with Not_found -> if Option.is_empty lev then user_err Pp.(str "A left-recursive notation must have an explicit level.") |