From d618791e00b0550b8e639bd63df451c2ab13805a Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 15 Dec 2002 12:10:18 +0000 Subject: Meilleure factorisation des entrées NEXT internes Nouvelle entrée "annot" pour contourner le conflit entre ">" et les annotations entre piquants MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3440 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/pcoq.ml4 | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) (limited to 'parsing/pcoq.ml4') diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 96b358402..33948d83b 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -351,6 +351,7 @@ module Constr = let global = make_gen_entry uconstr rawwit_ref "global" let sort = make_gen_entry uconstr rawwit_sort "sort" let pattern = Gram.Entry.create "constr:pattern" + let annot = Gram.Entry.create "constr:annot" let constr_pattern = gec_constr "constr_pattern" end @@ -506,7 +507,7 @@ let camlp4_assoc = function | Some Gramext.NonA | Some Gramext.RightA -> Gramext.RightA | None | Some Gramext.LeftA -> Gramext.LeftA -let adjust_level assoc = function +let adjust_level assoc from = function (* If NonA on the right-hand side, set to NEXT *) | (n,BorderProd (false,Some Gramext.NonA)) -> Some None (* If NonA on the left-hand side, adopt the current assoc ?? *) @@ -520,7 +521,10 @@ let adjust_level assoc = function if (left & a = Gramext.LeftA) or ((not left) & a = Gramext.RightA) then Some (Some n) else Some (Some (n-1)) (* | (8,InternalProd) -> None (* Or (Some 8) for factorization ? *)*) - | (n,InternalProd) -> Some (Some n) + | (n,InternalProd) -> + match from with + | ETConstr (p,()) when p = n+1 -> Some None + | _ -> Some (Some n) let compute_entry allow_create adjust = function | ETConstr (10,_) -> weaken_entry Constr.lconstr, None, true @@ -530,6 +534,8 @@ let compute_entry allow_create adjust = function | ETBigint -> weaken_entry Prim.bigint, None, false | ETReference -> weaken_entry Constr.global, None, false | ETPattern -> weaken_entry Constr.pattern, None, false + | ETOther ("constr","annot") -> + weaken_entry Constr.annot, None, false | ETOther (u,n) -> let u = get_univ u in let e = @@ -539,15 +545,16 @@ let compute_entry allow_create adjust = function let get_constr_entry = compute_entry true (fun (n,()) -> Some n) -let get_constr_production_entry ass = compute_entry false (adjust_level ass) +let get_constr_production_entry ass from = + compute_entry false (adjust_level ass from) let constr_prod_level = function | 8 -> "top" | 4 -> "4L" | n -> string_of_int n -let symbol_of_production assoc typ = - match get_constr_production_entry assoc typ with +let symbol_of_production assoc from typ = + match get_constr_production_entry assoc from typ with | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj) | (eobj,Some None,_) -> Gramext.Snext | (eobj,Some (Some lev),_) -> -- cgit v1.2.3