From 351e9acd3aa11a751129f5956fe991fc4d0bf0b8 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 11 Aug 2017 19:24:50 +0200 Subject: Introducing an intermediary type "constr_prod_entry_key" for grammar productions. This type describes the grammar non-terminal. It typically contains ETConstrList (now renamed ETProdConstrList) but not ETBinder. It is the type for metasyntax.ml and egramcoq.ml to communicate together. The type constr_prod_entry_key with ETConstr, ETBinder, is now used only in metasyntax.ml. This allows to get rid of some "assert false" in uselessly matching over ETConstrList in metasyntax.ml and of some "assert false" in uselessly matching over ETBinder in egramcoq.ml. Also exporting less of extend.mli in API. --- vernac/metasyntax.ml | 27 ++++++++++++++++----------- 1 file changed, 16 insertions(+), 11 deletions(-) (limited to 'vernac/metasyntax.ml') 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.") -- cgit v1.2.3